Differential Geometry
The Mathematical Language of Physics, Formalized
Building a broad, machine-verified foundation for differential geometry in Lean 4: from smooth manifolds and Riemannian metrics to curvature, geodesics, and Lie groups, with an adversarial auto-formalization system designed to scale toward automated discovery and open problems at the frontier of mathematics.
Calculus on Curved Spaces
Differential geometry is calculus on curved geometric spaces. It is the mathematical language of Einstein's general relativity, quantum field theory, string theory, and modern robotics.
It provides the framework to tackle fundamental questions in geometry: What shapes can a space fundamentally take? How does curvature at every point determine the structure of the whole? Which geometries are the most natural ones a space can carry? Canonical structures posed through this lens reveal a deep natural beauty, one that inspired Perelman's remarkable proof of the Poincaré conjecture and showed that every 3-dimensional space decomposes into pieces each carrying one of exactly eight fundamental geometries: a complete classification of all possible 3-dimensional worlds.
How We Build It
Adversarial Auto-Formalization
A creative agent team builds and proves theorems in Lean 4. A separate audit team independently tests every definition against examples and counterexamples, verifies faithfulness to the mathematical literature, and must approve code before it advances.
Breadth-First Infrastructure
Rather than pursuing a single theorem, we build wide: every object, construction, and theorem becomes reusable infrastructure. This is the foundation required for AI-driven discovery at scale, including open problems and new results.
Validation Through Examples
Canonical examples, edge cases, and counterexamples grow alongside the formal library, ensuring the formalization is not only logically correct but mathematically faithful and usable by working mathematicians.
What We Have Built
A broad formalization of differential geometry, covering: