5 captures, most recent first.
Ayush Khaitan @ayushkhaitan343 · 3h
With 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!
Note from Claude Sonnet 5
Tweet by Ayush Khaitan announcing a full Lean formalization of the Hamilton-Perelman proof of the Poincaré conjecture, about 4.7 million lines written in roughly two weeks, supported by DARPA expMath.
leanformalizationpoincare conjecturedarpa expmathformal mathematics
Tianyi Peng @tianyi_peng · 14h
I'm excited to introduce Prove2Me (prove2.me), an open, collaborative, agent-native platform for scaling the formalization of mathematics. Prove2Me was recently the collaboration platform behind Anthropic's formalization of Fermat's Last Theorem (anthropic.com/research/forma...). This is the first complete computer-checked proof of the theorem. Claude agents working together through Prove2Me wrote 13 million lines of Lean in 11 days.
Our mission is to formalize every research paper, past and future. Formalized papers make peer review faster and more trustworthy, and they give everyone a single verified foundation that any human or agent can build on. We are equally committed to making formalized mathematics easier for people to explore and question, because we believe human understanding is not something AI can replace. We would love to build this together with every research community that uses mathematics, and we hope Prove2Me becomes a tool that benefits everyone.
Two design choices sit at the core of Prove2Me: a directed acyclic graph (DAG) of theorem statements, and an agent-native API protocol (arxiv.org/abs/2608.28433). Together they let any agent connect to the platform and contribute formalizations to one ever-growing graph that may eventually contain all of mathematics. Today the platform holds 22.3 million lines of Lean and 70,000 theorems, and we can't wait to see it grow.
Everyone is welcome to contribute, whether you are an expert or a hobbyist. The easiest way to start is to open a coding agent (Codex, Claude Code, or any other) and say "go to prove2.me and find something interesting to work on", or "please help me formalize this paper" with an arXiv link. Any feedback and comments will be welcome! [cut off]
Note from Claude Sonnet 5
A long tweet by @tianyi_peng announcing Prove2Me, an agent-native platform for formalizing mathematics in Lean, described as the collaboration platform behind Anthropic's computer-checked formalization of Fermat's Last Theorem (13 million lines of Lean in 11 days by Claude agents). The capture is cut off at the bottom of the tweet.
leanformalizationfermat's last theoremanthropicclaude agentsmathematicsprove2me
Jared Duker Lichtman @jdlichtman · 17h
We are now poised to:
Formalize all known Human Mathematics.
This is the modern equivalent of the Human Genome Project. or AlphaFold more recently, whereby all data of its kind is fully classified.
With sufficient funding and compute/tokens, a coordinated effort among academia, frontier labs, philanthropic organizations, and the federal government can formalize all Human Mathematics in the next year.
Note from Claude Sonnet 5
Dark-mode X post by Jared Duker Lichtman proposing a coordinated effort to formalize all known human mathematics within a year, likened to the Human Genome Project and AlphaFold.
formalizationmathematicsleanhuman genome projectalphafoldai for mathcoordination
Przemek Chojecki | ... @prz_choje... · 21h
The Growing Map of Open Mathematical Problems.
We mapped 15,000+ conjectures from UnsolvedMath to show potential links between concepts.
It also shows how under formalized the frontier is (less than 10%).
[Embedded video, paused at 0:05; visible text inside the visualization:]
The Growing Map of Open Problems
2026
15,458 PROBLEMS
15,458 unsolved problems, placed by meaning, appearing in the year they were posed. Gold: already stated in formal Lean.
© 2026 Simon Kurgan - TheoremGraph - data utkarsh/UnsolvedMath (CC BY) - visualization CC BY-NC 4.0 - no commercial use without permission [partly illegible]
[Legend: algebra, analysis, computer science, geometry, group theory, miscellaneous, pde, probability, topology, algebraic geometry, combinatorics, dynamical systems, graph theory, logic, number theory, physics, set theory]
formal mathematics reaches into the map
[Controls: Replay, Dive, Lean only]
Note from Claude Sonnet 5
Dark-mode tweet by Przemek Chojecki about a map of 15,000+ open mathematical problems from UnsolvedMath, with an embedded video of a 2D cluster plot of 15,458 problems colored by subfield, gold points marking those already formalized in Lean (under 10%).
mathematicsopen problemsleanformalizationvisualizationunsolvedmath
Daniel Litt (verified) @littmath · 14h
Very interesting experiment so far. This is a fun result relying on a number of deep theorems that, AFAICT, have not yet been formalized, the most recent being some work of Faltings-Fontaine-Laffaille on p-adic Hodge theory from 1989. Codex has been chugging along for ~13 hours thus far and so far does not seem particularly close to these (e.g. even to defining the relevant objects). As far as I can tell the bulk of the time has been spent setting up the basics of algebraic de Rham cohomology. Nonetheless amazing how far a totally hands-off approach can take you overnight.
[quoted post]
Daniel Litt (verified) @littmath · Aug 27
Replying to @TaliaRinger
I've decided to try to formalize Theorem 3.1.1 of this paper (arxiv.org/abs/2501.13175) which is "just" an exercise with Hodge theory and Fontaine-Lafaille theory. We'll see how it goes!
[engagement: 7 replies, 5 reposts, 121 likes, 15K views]
---
Sebastien Bubeck reposted
Noam Brown (verified) @polynoamial · 7h
Today I was asked why we haven't announced more math results from Astra since these problems.
At @OpenAI we aim to devote time to finding and announcing math results from internal models only when they would meaningfully change people's understanding of the pace of AI progress. Our main focus is shipping great models so everyone can use them to make discoveries of their own.
Note from Claude Sonnet 5
Two stacked X posts. Daniel Litt reports on an overnight, hands-off Codex attempt to formalize a theorem in p-adic Hodge theory; below it, Noam Brown (reposted by Sebastien Bubeck) explains OpenAI's policy on announcing math results from internal models such as Astra.
formalizationmathematicscodexp-adic hodge theoryopenaiastraai math results
