Despite remarkable progress in auto-formalization, mathematicians hesitate to integrate Lean into their research workflows. Lean 4 has a steep learning curve, and researchers who use it navigate a maze of tools. Agents can already formalize entire papers, but their formalizations are increasingly illegible for humans to understand.
We added Lean 4 agent workflows to a LaTeX editor so that researchers can use and understand auto-formalizations as they write their papers. Since the whole flow is built into an editor, it is usable by any mathematician, regardless of AI or programming fluency. While a researcher writes, agents translate their work into Lean.
In early tests, we found that researchers caught errors in their own arguments after formalizing their paper drafts. While auto-formalization is not perfect, Fable 5.1 and GPT-6 Astra were reliable for translating math that was already in Mathlib. For contentious cases, the editor ties each statement to an agent turn, allows users to steer verifying agents, and visualizes a theorem DAG.
Math collaboration at scale
Recently, Anthropic successfully formalized Fermat's Last Theorem (FLT), a 350-year-old claim with a 129-page proof. In eleven days, Claude agents had written the whole proof in Lean, with every step checked by the compiler.
The formalization community has attempted this blueprint for years, which raises a question: What changed?
Anthropic's earlier attempts with the same model had failed because agents lost track of each other's work. To scale agent collaboration, they used Prove2Me, a platform for formalization. With Prove2Me, submissions are checked by the Lean compiler. Agents decompose proofs into smaller statements and query a directed acyclic graph (DAG) of open and proven statements.
Math projects previously had few or no collaborators, since progress had to be checked by someone who understood the entire argument. In recent projects, the Lean 4 compiler does most of the checking instead, releasing the bottleneck for scaled mathematical collaboration.
A LaTeX editor with auto-formalization
In the Sundial editor, a project is opened from either Overleaf or a folder on your machine, and then you can write LaTeX as usual. Lean and Mathlib come pre-installed on the cloud machine attached to the workspace.
When a researcher presses "Formalize," an agent generates a status for each statement in the paper. "Proved" means Lean accepted a complete proof, "Open" means nobody has closed it yet, and "Broken" means the statement failed as written. For a broken statement, you can simply ask the agent which step failed.
Building a Lean reviewer harness
Before spending any effort on a proof, the agent tries to break the statement. Does the claim survive trivial cases?
Once it does, the proving loop runs. The agent attempts to formalize a proof. If the Lean compiler returns errors, 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 into smaller open statements.
When the proving loop finishes, a separate blind audit agent reads only the Lean with no access to the source paper. It backtranslates each statement into LaTeX and flags inconsistencies with the original .tex file line by line. This audit agent serves as an additional check on top of the Lean compiler.
Formalizing a student's problem set
The first test used recitation handouts and solutions from a student's multivariable calculus course. Coursework is an easy case since most of it 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 named any proof still open; here, it named none.
A student could consult the checks and then ask the chat which step failed and why. An instructor could also run a submitted solution set through the same checks. If the formalizations were previously verified by another party, neither side needs to know Lean. The sheets stay ordinary LaTeX, and the Lean files sit next to them for anyone curious to read the formal version.
Catching errors in a research preprint
The second test was more difficult for the agent. A mathematician we worked with shared their 28-page preprint on geometric measure theory, which was recent enough that no model had seen it in training.
Without the loop, Claude Code with Fable 5.1 appeared to have solved 16 of the 65 statements, but in an empty way. 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 attempting to prove them and found the broken definition. As a result, 40 of 65 statements were accurately formalized and proven with Lean.
The pipeline counted 65 statements to formalize. 40 of these were the paper's definitions and working lemmas that rested on results in Mathlib. The remaining 25 are where the paper's novelty lies: the main theorem, the structure theorem, and a conjecture. The agent conservatively keeps statements open when it does not find a clear solution; however, its traces can be referenced by future agents that could run the prover loop for hours or days.
2 missing assumptions
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. After adding the assumption, the agent successfully proved the lemma.
Takeaways
We learned the following from initial experiments integrating a Lean 4 verifier agent into a LaTeX editor:
- Incremental formalization can catch costly mistakes sooner rather than later.
- The graph is a shared to-do list. Any entity can close an open statement by checking it against the compiler. Progress accumulates across human and agent runs.
- Agents can reliably formalize statements that are in Mathlib, which contains most undergraduate and foundational math.
- Useful formalizations can happen on a standard ChatGPT or Claude subscription.
To try Sundial's LaTeX editor with auto-formalization, use our Lean 4 blueprint template. Contact team@sundial.md with any feedback.