In spring 2026, while working on my Bachelor’s thesis on automated theorem proving with AI, I spent almost two months building Formalizer. The idea was simple: upload a mathematics paper, translate it into Lean, and find out whether it was correct.
Lean is a proof assistant that mechanically checks proofs written in its formal language. In our thesis experiments, even relatively inexpensive models could prove difficult, already-formalized theorems. I wanted to take the next step: start with a paper instead of a prepared Lean statement.
I got as far as toy examples. Along the way, I built several interfaces, changed the architecture repeatedly, and eventually deleted much of it.
What Lean actually guarantees
My original plan was a mathematical oracle: PDF in, verified Lean project out, with a verdict on the paper.
The problem is that proving a statement and translating it faithfully are different tasks. An agent can add an assumption, omit a case, or choose a definition that changes the meaning. Lean can then check a perfectly valid proof of the wrong theorem. Failure to find a proof is equally inconclusive: the paper might be correct and the agent simply stuck.
This meant I needed someone who understood the mathematics to review the translation. But asking them to inspect a large, messy AI-generated Lean repository did not seem much easier than asking them to construct the formalization themselves.
I borrowed an idea from collaborative formalization projects: a blueprint, a human-readable account of the definitions, lemmas, and proof steps, linked to Lean declarations and organized as a dependency graph. Terence Tao’s tour of a blueprint explains the approach through a real project.
In Formalizer, each node held an informal statement, a proof strategy, and its dependencies. A human could inspect the mathematical structure before reading the Lean translation. Agents could use the same graph to divide the work and prove nodes in dependency order.
Review does not fit into three phases
I initially planned three stages, with human approval between them: build the blueprint, translate its statements into Lean, then prove them. Catching mistakes early mattered because even small theorems could burn many tokens on reasoning, library search, compilation, and retries.
But some bad translations only became apparent during proof attempts. A definition could compile yet be awkward to use with Mathlib, Lean’s mathematics library. Fixing it could force changes to several later statements. The workflow needed to move backwards, and my state machine kept growing to accommodate that. I kept redesigning the workflow, but I hadn’t formalized enough mathematics myself to know which design would work.
I started thinking of the project as a “Cursor for mathematicians”: a tool where the user could inspect the graph, edit statements, and ask agents to work on individual nodes. I built a web UI around this idea, hoping the blueprint would make reviewing the agent’s work easier.
Letting agents edit
One design change was especially useful. Initially, agents returned candidate files as structured output, and only the orchestrator could write them. This gave me control over changes, but put the orchestrator in the middle of the agent’s edit–compile–inspect loop.
I switched to isolated git worktrees. An agent could edit real files, invoke Lean, and retry inside its own checkout. Its work could then be validated and reviewed as a diff before merging into the main project.
Compilation was only one check. Validators also restricted which files could change, rejected remaining proof placeholders, and checked that a proof agent preserved the approved theorem statement. Otherwise, it could make its task easier by changing what it was supposed to prove.
I then built a proof-of-concept GitHub App to review changes through pull requests. That gave me another interface to maintain before I’d managed to formalize a real paper.
Removing most of the application
As my thesis deadline approached, I tried to get the full pipeline working reliably. Managing the context and prompts of many specialized agents had become a problem of its own. Orchestration kept breaking on edge cases.
I removed the web UI, terminal UI, GitHub integration, background jobs, and several agent roles, leaving a small CLI. I also changed statement formalization from separate per-node operations to one project-wide pass: independent agents chose incompatible representations, or needed to read the whole project anyway. Once the shared definitions and statements were in place, proofs could still be attempted individually.
The remaining workflow was:
It could parse and formalize some toy examples end to end. The surviving test uses a small theorem about two-step paths in a graph on natural numbers. I never completed a real paper, and I never established that the pipeline was meaningfully better than one capable coding agent with access to Lean.
I also wasn’t sure who would use it. The reviewer needed enough mathematical and Lean knowledge to judge the translation. Those users already had ways to work on formalizations; I had not shown why they would prefer mine. At that point, I stopped.
I still think the blueprint was worth exploring. If I restarted, I would first work through a small formalization myself, with a coding agent, and study how existing projects were organized. Only then would I try to automate parts of that work and compare the result against the simpler workflow.