A Saturday reflection on imagining a geometry of axiomatic systems and wondering whether theories could become types that carry information about what can and can't be proven about them, inspired by proof assistants like Lean.