Love this. Via @patrickshafto and @DARPA's expMath program, @ayushkhaitan343 announces:
"With Ben Chow, Yuan Liao and Ziyang Qin, we have completed a full Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture!"
For context on expMath and in @r0ck3t23 words over at x.com/r0ck3t23/statu…
"DARPA has just kicked off Exponentiating Mathematics (expMath), a three-year program aimed at radically accelerating pure math research by developing AI that can propose and prove abstractions. According to the official program brief, expMath will bring together teams focused on auto-decomposition; automatically breaking complex conjectures into reusable lemmas; and auto(in)formalization, bridging the gap between human-readable mathematics and rigorously checked proofs in languages like Lean."
Quoting @ayushkhaitan343 · Sep 27, 2026With Ben Chow, Yuan Liao and Ziyang Qin, we have completed a full Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture!
The proof is around 4.7 million lines of code, written in roughly two weeks. Grateful to the @DARPA expMath program for its support!
X (formerly Twitter)Dustin (@r0ck3t23) on XDARPA’s expMath: Turning AI into True Math Co-Authors
DARPA has just kicked off Exponentiating Mathematics (expMath), a three-year program aimed at radically accelerating pure math research by developing AI that can propose and prove abstractions. According to the official program brief, expMath w…↗ x.com