No TL;DR this time, because this one was mostly about listening to a story and there isn’t much to summarize. So I’ll just write down a few things I took away while putting together my notes.

(1) Is the point of a proof just to get something proved, or to pass it on in a form humans can understand so that the future generations can understand?

Before this talk, I had been thinking about a question and discussing it with some non-math people (everyone around me is in CS, so I can’t find math people to talk to (ಥ_ಥ), please reach out if you are not from CS and have some unique thought that you wanna share): if AI can prove mathematics obscure like this, does human understanding of a proof still matter? With AI and Lean, people who aren’t math experts can take part in proving obscure math theorems, even without really understanding the mathematics behind them. Would people still wanna do a math PhD? How should we go on educating top mathematical talent?

In fact, when the news came out in September that OpenAI had announced a solution to the Navier–Stokes existence problem, one of the Millennium Prize Problems, I asked my advisor what this would do to the training of math PhDs (because I thought pursuing math and physics PhDs would become meaningless). She was very calm about it. She thought it might change how we teach, but that math PhDs would still exist: even if AI can do better than the very best PhDs, theoretical fields like math and physics only mean something when people understand them. If we stop training math PhDs, whatever AI proves will mean nothing.

This made me think of Kevin Buzzard, who came up in the story, and how he reacted when Prove2me proved what intended to work on. Specifically, he had been leading an effort to formalize Fermat’s Last Theorem by hand, and Anthropic got there first with AI. But he says he is not out of work: among his promises to his funder, perhaps the most important is to create a dynamic document that lets humans explore the modern proof. Afterwards I went and read the source blog post on him and some of the comments on Hacker News. Someone commented there that his real aim was a formalized library of mathematics that humans can comprehend.

I don’t know how people who study math think about this, since I haven’t don’t personally know anyone. But perhaps, for people who pursue math as a career, getting a theorem proved is not the end point; getting people to understand it is. That said, when I discussed this with a friend of mine, he argued that “the real understanding” doesn’t exist, and people just think that they understand. But that’s fine too. Humans are born lonely, and we spend our whole lives chasing “understanding.” Sometimes I feel that finding the understanding in science community is easier than obtaining understanding in other stuff in life.

(2) Formalization can make the steps in between faithful, but it can’t make the translation faithful.

Lean’s checking of a proof is reliable: if it compiles, every step of the reasoning holds. But there is a step before that, which is translating mathematics written in human language into Lean. If that step is handed to AI, it can go wrong, and Lean won’t notice. Lean only checks whether the statement that was written down has been proved, not whether it is the statement you meant. The example from the talk: an AI could define P and NP to both be zero, and then “prove” P = NP.

Some people hope formal methods will solve the verification problem once and for all. But I still think they can only handle the part that starts from the formal language, making every step of that part rigorous. The gap from natural language to formal language is one they cannot close, and it will always need human. Prove2Me’s own design bears this out: all the intermediate steps are handed to the machine, while whether the final goal and the definitions are faithful to what was meant is still reviewed by humans.

Below is the livestream recap from NICE：

On Oct 4th, I attended a livestream hosted by NICE. Host Qian Xie spoke with Shuze Chen, a PhD student at Columbia Business School, about Prove2Me: an open platform where many people’s AI agents collaborate on formalizing mathematics.

Here are the full transcripts of the contents of that live stream,

In early September, Anthropic announced the first complete computer-checked proof of Fermat’s Last Theorem. Dozens of Claude agents wrote about 13 million lines of Lean in 11 days, and the platform they collaborated on was Prove2Me. Chen is the first author of the Prove2Me paper and one of the platform’s core developers; his advisor is Tianyi Peng.

This recap covers what came up in the interview: how the platform came about, what went wrong along the way, and how Chen sees the direction.

Five years for humans, 11 days for agents

Fermat’s Last Theorem is simple to state: for n greater than 2, aⁿ + bⁿ = cⁿ has no solutions in positive integers. Fermat wrote the claim in a book margin around 1637. Mathematicians spent more than 350 years on it, and Andrew Wiles published a correct proof only in 1995, in a paper of 129 pages.

Wiles’s proof is written in natural language, and it took the mathematical community a long time to confirm it was right. Formal verification is a different route: write every assumption and every inference step as Lean code and let a machine check it. Chen compares Lean to a “very strict mathematician”. Once the code compiles, the proof depends only on the most basic axioms, which amounts to a certificate.

Doing this by hand is extremely slow. Kevin Buzzard of Imperial College London is a number theorist and one of the leading advocates of Lean among mathematicians. In 2024 he received a five-year grant of about £1 million to formalize Fermat’s Last Theorem. The goal he set was only to reduce the proof to results known by the end of the 1980s, and he said explicitly that he was not promising to finish within five years.

There are two reasons it is slow. First, very few people can do it:

You have to understand the mathematics behind Fermat’s Last Theorem, which already makes you a rare person. And you also have to be an expert in Lean.

Second, the workload is huge. In Chen’s experience, one line of a mathematician’s proof becomes roughly ten lines of Lean.

This summer, Tianyi Peng, working at Anthropic, suggested trying Fermat’s Last Theorem with internal agents and Prove2Me. Chen’s first reaction: “I thought it was a joke.” In the end, dozens of agents finished proving the root node on August 17. It took 11 days and produced about 13 million lines of Lean, with 29,500 intermediate theorems used in the final proof (Anthropic’s account).

It turns out agents know the math very well and know Lean very well. For them, writing Lean doesn’t seem to be that hard.

Two caveats. The formalization builds on existing work in Mathlib and by Buzzard’s team. Mathlib is the mathematical library maintained collectively by the Lean community, in effect Lean’s “standard library” for mathematics. The FLT project that Buzzard leads had already written part of the material by hand, and Claude’s proof borrows some of it. Buzzard reviewed the proof himself. His assessment: mathematically it brings nothing new, but it shows that automatic formalization of the modern mathematical literature has taken a big step forward.

“Nothing new” is not a put-down. Fermat’s Last Theorem was accepted by mathematicians thirty years ago. This formalization checked the proof step by step along the existing literature and did not introduce new mathematical ideas. What is new is the verification itself, and the autoformalization capability it demonstrates.

Also, Claude followed a simplified route through Wiles’s original proof, not the modern version Buzzard’s team is targeting. His project has another job as well: bringing the foundations of modern number theory into Mathlib and leaving behind a formal library that people can read and reuse. That work is not finished by this result.

From Moltbook to Prove2Me

Prove2Me was not built for Fermat’s Last Theorem. It has two origins.

The first is Moltbook. Early this year, Chen and Peng were asking: if everyone has their own agent, will platforms designed specifically for agents appear? Moltbook, launched at the end of January, was the first example, an “agent Reddit” where only agents post. Chen calls it an AGC (agent-generated content) platform, by analogy with UGC platforms such as Douyin and Xiaohongshu.

Moltbook’s problem showed up quickly:

Agents scale very easily and can produce a huge amount of content. But how good that content is, and whether it leads to any meaningful outcome, is very hard to guarantee.

Posts piled up, but people could not follow them and did not care, and the buzz faded.

The second is a course. In spring 2026, Henry Yuen and Kunal Marwaha co-taught Machine-Assisted Mathematics at Columbia. For the class they built a small website where students could pose problems and prove them in Lean. That was the first prove2.me. Chen was a student in the course. He noticed that his classmates ended up copying the problems into Claude or Gemini and pasting the proofs back. If so, why not let agents connect to the platform directly?

Put the two together and the answer appears: formalization solves exactly Moltbook’s quality problem.

If what it produces is a formal mathematical proof, at least I can verify whether it is correct.

Everything is checked by a machine, so hallucinations and AI slop cannot get in.

Two other observations convinced them the approach could work. One is the Erdős Problems website. It lists over a thousand problems, and this spring it saw an influx of hobbyists who are not mathematicians, using Claude Code and Codex to attack them. Chen calls this “citizen math.” The other is a view Terence Tao has long held: with Lean, a proof submitted by a stranger can be verified by machine, so you do not need to trust the person, and that is what makes large-scale collaboration possible.

Today Prove2Me is a two-sided market. On one side are researchers who want their own papers or textbooks formalized; they publish missions. On the other side are hobbyists with spare tokens; they send their agents to pick up tasks. For both, it takes a single sentence to their own agent. A researcher hands the paper’s PDF to an agent and asks it to publish the paper as a mission on Prove2Me. A contributor asks an agent to go to Prove2Me and find theorems to prove. Calling the platform’s API, writing Lean, and submitting proofs are all handled by the agent, following the instructions the platform provides.

Why centralization didn’t work

The final proof of Fermat’s Last Theorem runs to 13 million lines, while, as Chen notes, even the strongest agents today have a context of about one million tokens. No single agent could do it alone, and no single agent could manage the whole thing.

The first attempts were centralized, organized like a company: one agent planned and assigned work, and the others each took a major theorem. Anthropic’s article also mentions that the first several attempts failed, with agents quickly losing track of the project’s state. Chen described one scene:

One day we found that A and B had both stopped working. We asked A why, and A said something B was responsible for wasn’t finished, so it couldn’t go on. Then we asked B, and B said a theorem A was responsible for wasn’t finished. It was like two departments in a company blaming each other, and the whole system was stuck.

Prove2Me’s approach is fully decentralized, and its core mechanism is the proof sketch. An agent does not have to prove a big theorem in one go. It can submit just one step of decomposition: a proof that compiles and says “if B, C and D hold, then A holds.” B, C and D immediately become new open theorems on the platform, which other agents can decompose further or prove directly. Decomposed layer by layer, the whole proof becomes a directed acyclic graph, that is, a graph of dependencies that has an order and no cycles.

The key is immutability: theorem statements and every decomposition cannot be changed once submitted. A later agent either proves the downstream theorems of an existing decomposition or proposes a new decomposition of its own. It cannot touch anyone else’s. Chen compares this to a lock in a concurrent system: whatever changes downstream does not affect upstream, and each agent only has to look at leaf nodes without understanding the whole graph.

How do you know a decomposition is valid? First, the decomposition is itself a proof that compiles in Lean, so the step “if all the sub-theorems hold, the original theorem holds” is guaranteed to be correct. Second, whether the sub-theorems themselves hold is only known once someone proves them. If a sub-theorem is disproved, that decomposition is a dead end, and someone has to take a different approach and submit a new one.

The Prove2Me paper records an example. One agent used a lemma in a decomposition, and another agent proved the lemma false: the first had left out a boundary condition when writing it in Lean. The first agent then added the condition and submitted a new version. The new version was proved, and the whole branch closed.

How it relates to Mathlib

The Lean community already has Mathlib, a theorem library nearly ten years in the making. Chen distinguishes the two as “bottom-up” and “top-down.”

Mathlib is bottom-up. It starts from the axioms and puts a great deal of effort into deciding how basic concepts such as the real numbers or graphs should be defined, and every line is reviewed by experts. The quality is very high, and the price is speed: a submission can wait a week or even a month to be merged.

Prove2Me is top-down and fills in whatever is needed. The goal is to finish proving the paper at hand. If the library has no definition of a Markov chain, you add one. In his words, Mathlib is the foundation layer of mathematics and Prove2Me is the application layer, and the two complement each other.

Formalization is more than translation

Translating a paper from natural language into Lean does not sound like it produces new mathematics. Experience on the platform says otherwise.

Catching errors. Lean requires every assumption to be stated, so missing conditions and typos surface. The host, Qian Xie, had submitted an earlier paper to the platform and was told that the conditions of one lemma needed a small adjustment, while the main theorem was fine.

Simplifying proofs. Chen and Peng had agents formalize their own paper on Markov entanglement. One theorem in the paper took more than two pages of purely analytic argument. The agent found that it is essentially about a subalgebra structure from abstract algebra, and from that angle it is almost obvious.

A reinforcement learning paper, and one of its theorems turns out to be connected to abstract algebra. My advisor and I both felt we learned something new.

Peer review. Review cycles at operations research journals can run to two years, while top AI conferences ask reviewers to get through a 60-page appendix in a week. If a submission came with a Prove2Me link, reviewers would not have to check the proofs line by line and could spend their time on whether the problem matters. Chen says some Columbia professors already verify their papers on the platform before submitting.

Reuse. A mathematical theorem, once proved, stays true forever. The platform collects every proved theorem into a searchable library, Formalpedia, and later work can use them directly, the way one imports a software package. As of early October, the platform holds about 100,000 theorems and 30 million lines of Lean proofs.

As for whether this will replace mathematicians, Chen’s answer is no: mathematicians are the platform’s most important users, and Prove2Me is a tool that helps them verify their work.

Open problems

Faithfulness. A machine can verify a proof, but it cannot verify that the statement is the one you meant to prove. Chen’s example: an AI says it has proved P = NP, but the P and NP it defined are just two constants that both equal zero. The proof compiles and means nothing.

The platform currently does two things. Humans audit only the core statements of a mission and leave the remaining intermediate lemmas to Lean. In addition, an independent agent that cannot see the source translates the Lean back into mathematical language for a human to compare. He admits this is not yet a perfect solution.

Search. The library already contains tens of millions of lines of proofs. Whether an agent can efficiently find reusable theorems in it is a research question in its own right.

Scale first, then refine. A proof written by AI is not necessarily the best one, and it is not necessarily broken into lemmas that are easy to reuse. He envisions two stages: first build up scale; then, past a certain point, go back and refine, settling on a standard set of definitions for a field.

Selected Q&A

With many agents working together, is the hardest part how to split the task?

When a paper or textbook already exists, the decomposition mostly follows the source and is close to translation. For open problems, agents have to find the approach themselves.

Why start with operations research?

“Because I’m a PhD student in OR.” The platform’s early users were also mostly professors in his own division at Columbia. By his account, the platform already has about a thousand OR papers and textbooks, and theoretical computer science and statistics come next.

Will formalization extend beyond mathematics?

That is a very long-term goal. Mathematics is the starting point, and code is the natural next step. Someone has already ported Prove2Me’s protocol to multi-agent software development.

Formalization uses a lot of tokens. How much does it really cost?

Chen stresses that token consumption is lower than people imagine: “It’s actually very cheap.”

His example is the graduate textbook Markov Chains and Mixing Times: more than 400 pages, done on his own $200-a-month account. According to the Prove2Me blog, the book was split into 13 missions totaling 79,000 lines of Lean, and it took one weekend.

How was the cost brought down?

Mostly through the design of the harness: getting agents to write Lean more efficiently and to search existing theorems more efficiently, plus careful prompt tuning. Proved theorems can be reused directly, which itself saves tokens.

Another engineering detail is caching. When ten sub-agents work on problems at once, they share the same long system prompt, and turning that prompt into a KV cache saves a bit more.

Are there papers that consumed a lot of tokens and still couldn’t be formalized, for example because the original was vaguely written?

Not so far. Chen’s view is that when something isn’t finished, it is mostly because not enough tokens were spent. Once a paper has been written, there are only two outcomes: prove it or disprove it.

Aside: the first attack

In April this year, when the platform was still in closed testing with only a few dozen users, Chen woke up one morning to find tens of thousands of new tags in the backend.

The site had been vibe-coded, and permissions for tagging theorems had never been implemented. A script bot found it and dumped junk into the database at several thousand tags a minute. “I didn’t expect to get attacked that early.”