Despite remarkable progress of agents formalizing and proving theorems in Lean, mathematicians hesitate to integrate AI-assisted formalization into their research workflows. Lean has a high learning curve, and the few researchers who use it work through a maze of tools. Harnesses that can formalize entire papers exist, but they've not yet been placed in the editor where a researcher writes.
We built formalization into a LaTeX editor so Lean 4 agents can work on your paper alongside you and your coauthors. Everything they add is checked by the Lean compiler, and the whole flow is usable by any mathematician regardless of AI or programming fluency. A researcher writes as usual, or brings in an existing paper, and in the background agents translate the math into Lean and prove what they can. As you write, your work gets checked.
Collaboration at scale in mathematics
Last week, Anthropic used AI agents to formalize Fermat's Last Theorem (FLT), a 350-year-old claim with a famously long proof. A community of mathematicians had been working to complete this blueprint for the last decade. In eleven days, Anthropic's agents had written the whole proof in Lean, millions of lines, every step checked by the compiler.
Academia and AI labs alike have attempted this blueprint for years, which raises the question: What changed?
Capabilities have increased with every model generation, but this is not the only improvement. Anthropic notes that earlier attempts with the same model had failed because agents lost track of each other's work. The final leg of work was to improve the scaffolding for scaled agent collaboration. They used Prove2Me, a platform where proofs are decomposed into smaller statements, every proof is checked by the compiler instead of the model itself, and agents query a directed acyclic graph (DAG) of what was proved and what was still open.
Claude agents could work for days on FLT because every statement lived in one theorem graph that any agent could read and update. When a proof attempt fails, an agent proves what it can and states the missing pieces as new open statements. Lean checks that this reduction is sound, and the graph stores the statement as proved except for those pieces.
Math projects previously had few or no collaborators, since contributions had to be checked by someone who understands the whole argument. In Terence Tao's Equational Theories Project, the Lean 4 compiler did the checking instead. As a result, there were fifty contributors working on the same project. The bottleneck for scaling mathematical collaboration was verifying contributions by hand.
A LaTeX editor with auto-formalization
In Sundial, a project is opened either from Overleaf or a folder on your machine, and then you can write LaTeX as usual. There is nothing to install: Lean and Mathlib, the main Lean 4 community library, already run on a cloud machine attached to the workspace.
After you click "Formalize", a few minutes later each statement in your paper has a status. "Proved" means Lean accepted a complete proof, "Open" means nobody has closed it yet, and "Broken" means the statement fails as written. Result dependencies are visually displayed in the editor. When one is broken you ask the chat which step failed. If the project is simple enough to formalize, you never need to open a Lean file.
How the loop works
When a researcher clicks "Formalize", the agent does not look proofs up. It writes each proof the way you would at a whiteboard. It unfolds the definitions, picks the idea, writes the steps. If a fact already exists in Mathlib, the agent recalls the lemma name from its weights. If the compiler says that name does not exist or does not fit, it searches the library for the right one and tries again.
Before proving, the agent tries to break the statement
Before spending any effort on a proof, the agent tries to break the statement. Do the assumptions even hold? Does the claim survive trivial cases?
If it does, then the proving loop runs. The agent writes a proof, the Lean compiler returns errors, and the agent tries again until the Lean check passes. When a statement fails multiple times, the loop marks it open and attempts to decompose it, surfacing the missing pieces as smaller open statements.
At the very end, a separate blind audit agent reads only the Lean, with no access to the source paper. It writes back what each statement says in plain language, and flags inconsistencies with your tex line by line.
Lean checks the proof, not the translation: a proof can be flawless while the Lean statement says something different from your paragraph. That is why the audit agent never sees your paper. An agent that can see the goal will write a reading that matches it. Turning formal proofs back into prose that people can read and believe is an old thread in verification; a compiler's check adds trust but does not replace the reading, discussing, and believing that make a proof accepted.
An initial test on a student problem set
The first test was on a student's multivariable calculus course, containing recitation handouts and solutions. Coursework is an easy case since almost everything it used already lives in Mathlib.
We pressed Formalize on two handouts: one on dot and cross products, and one on velocity, acceleration, and arc length. The agent translated more than sixty statements and definitions into Lean and proved them. Each Lean file ended with a compiler check that names any proof still open; here it named none.
For the student, they can reference the checks to then ask the chat which step failed and why. None of it requires knowing Lean. The sheets stay ordinary LaTeX, and the Lean files sit next to them for anyone curious to read the formal version.
For the instructor, they may run a submitted solution set through the same checks.
A smoke test on a research preprint
The second test was more difficult for the agent. A mathematician we worked with shared their new preprint, 28 pages of geometric measure theory, which was recent enough that no model saw it in training. The pipeline counted 65 statements to formalize.
Without the loop, Claude Code with Fable 5.1 appeared to have solved 16 of the 65 statements, but it was empty and incorrect. There were no real proofs, and one definition was encoded incorrectly. This incorrect definition made some assumptions impossible to satisfy, and an external prover "proved" 22 theorems on top of it.
With the loop, the agent adversarially attacked the statements before proving, and found the broken definition. As a result, 40 of 65 statements were accurately formalized and proven with Lean, and two missing assumptions found in the paper.
The 40 statements were the paper's definitions and working lemmas that rested on results in Mathlib. The 25 remaining ones are where the paper's novelty is: the main theorem, the structure theorem, and a conjecture. Mathlib did not have those yet, so prover runs take hours or days from that point onwards.
The inconsistencies it found
The agent found two missing assumptions in the paper: one lemma needed the angle to be less than 90 degrees, and one remark needed the weights to be whole numbers rather than fractions. Papers skip assumptions like these all the time. A compiler does not. With the assumption added, the agent proved the lemma. The agent flagged both and suggested the fix, without touching the paper.
Takeaways
- The graph is a shared to-do list. Anyone can attempt to close an open statement and check it against the compiler. Progress accumulates across people and agent runs.
- You do not need to wait until a paper is complete to formalize it. It runs while you write, so a mistake shows up the day you make it.
- Formalization involves translating your statements into Lean, and proving them. The translation takes minutes and already catches errors; proving takes minutes for lemmas that exist in Mathlib, and hours or days for novel proofs.
- Mathlib carries most of undergraduate and foundational math, and it grows every week. We wired its weekly update into the pipeline, so more of your paper proves itself over time.
- Research proofs can run for hours or days on a standard ChatGPT or Claude subscription.
- Research is about discovering whether an idea survives scrutiny. Formalization may shorten that time to hours, before you have built months of work on top of it.
We are rolling the pipeline out inside the Sundial editor. Bring a paper, press Formalize, and read the checkmarks. To start from a working setup, open the Lean 4 blueprint template.