LLMs’ mathematical breakthrough is another vibe coding moment, this time for Lean

In the last few months, frontier labs have announced a series of mathematical discoveries. In May, OpenAI shared their proof to the 46th Erdős problems. In July, Levent Alpöge, an Anthropic employee shared his discovery using Claude Fable 5 to disprove Jacobian conjecture. On the first day of August, OpenAI announced that they used their next generation model to solve 10 high-level questions in mathematics and computer science, each with a token budget of merely ~$2000.

These proofs arrived in different shapes. Alpöge’s counterexample spread as a single tweet, cross-checked by Wolfram Alpha and a handful of other models. OpenAI’s May proof arrived as a preprint, subject to peer review. Their August announcement, however, added something to the paper: a Lean certificate for each of the ten results — a machine-checkable proof written in formal language.

Back in school, we learned most proofs in natural language. They are concise and expressive, but often leave definitions implicit or routine steps unstated. Checking such proofs—especially for frontier problems—requires expert readers to reconstruct the argument and decide whether every gap is justified. A formal proof leaves no such gaps, making it possible for a computer to quickly verify.

And that’s not the whole picture: if the computer can tell if a proof is valid, it can also find proofs itself. The idea of Automated Theorem Proving (ATP) dates back to the 1950s and produces tools like SMT solvers (z3). More recently, interactive provers such as Rocq (formerly Coq) and Lean have taken hold, where a human directs the proof construction while the machine fills in routine steps and checks.

The same machinery underpins formal verification in software. Software engineers want programs to comply with their specifications, and a formally verified program has that compliance mathematically proved: the specified class of bug cannot exist. It is a remarkable technology, and a largely unused one. Even in avionics, chip design, and cryptographic implementations, it covers only the most critical fraction of a system, with testing carrying the rest. The reason is painstaking human effort, starting with translating a natural-language statement into formal syntax, then proving.

Language models may finally be what scales this up: they’re now formalizing arguments, breaking statements into subgoals, and searching for the right proofs. The timing is what makes this interesting. The same models that make verification cheap are also flooding the world with codes and arguments that no one has the capacity to check. As that volume rises, there is real reassurance in knowing that code has been mathematically proved correct, rather than merely tested.

In this post, I will briefly explain how AI models prove mathematical statements, using systems from major players such as Google DeepMind and ByteDance as examples. Many academic groups and companies are working on this problem; the systems discussed here are not an exhaustive survey, nor necessarily the state of the art on every benchmark. My aim is to lay the foundation for future posts on how formal verification is used in software design, who the main players are, and what recent mathematical breakthroughs teach us about LLMs.

Lean

To understand how AI uses interactive provers to prove mathematical theorems, it’s worth asking how Lean itself works — and to see that, it’s easiest to first watch a human use it. AI provers are, in the end, automating this same loop.

Lean is programming language built upon a dependent type theory known as the Calculus of Inductive Constructions. In everyday programming, a type such as int is often fixed and cannot refer to any particular value. Dependent types lift that restriction: the statement 2 + 2 = 4 is itself a type, and so is 2 + 2 = 5. The difference between the two is that the first is inhabited — there exists a term of that type, which serves as a proof — while the second is empty. To verify the proof, we only need to use Lean’s small kernel to check that the term’s type is indeed 2 + 2 = 4, thereby reducing reasoning-oriented proof checking to a more mechanical type checking.

To prove a mathematical statement in Lean, we must first translate it into Lean’s formal language—a process called formalization. Here is Lean code that states, but does not yet prove, that there exists infinitely many prime numbers:

theorem exists_infinite_primes (n : ℕ) :     -- 1
	∃ p, n ≤ p ∧ Prime p := by               -- 2
  sorry                                      -- 3 
  

1. (n : ℕ) declares a natural number n. It enters the local context — the list of things you have available — and shows up as the line n : ℕ in the proof state below.
2. ∃ p, n ≤ p ∧ Prime p is the proposition to be proved: “there exists a p that is at least n and is prime.” The := by says the proof that follows is written in tactic mode, which will be explained below.
3. sorry is a placeholder that unconditionally admits the current goal.

sorry is a unique placeholder in Lean. When it appears, Lean still compiles the code (with a warning), and displays the proof state: the established local contexts and the remaining goals. In this case, the proof state looks like this:

n : ℕ                    -- local context: something we know, also called hypothesis
⊢ ∃ p, n ≤ p ∧ Prime p   -- the goal we try to prove, also the type of the proof.

As we mentioned earlier, a statement can be proven by constructing a term that inhabits the corresponding type. Rather than asking users to construct these terms by hand, Lean offers a higher-level ‘tactic mode’. Tactics are commands — intro, apply, rw — — the basic unit of action in Lean, each one a move that acts on the proof state.

Suppose we borrow the central idea of Euclid’s proof: form $n! + 1$ and take its smallest prime factor as a candidate prime larger than $n$. In Lean, we introduce that candidate with the tactic let, which extends the context without touching the goal:

theorem exists_infinite_primes (n : ℕ) :
    ∃ p, n ≤ p ∧ Prime p := by
  let p := minFac (n ! + 1)  -- minFac x is the smallest prime factor of x.
  sorry

The tactic yields us a new proof state:

n : ℕ                     -- existing hypothesis in the local context
p : ℕ := (n ! + 1).minFac -- new hypothesis in the local context 
⊢ ∃ p, n ≤ p ∧ Prime p    -- the same goal

The goal is still there, and the good news is that we have new hypothesis in the local context, that if we apply more tactics, the goal will be closed. Stacking enough of them reaches a no-goals state — where the proof is complete.

This is the interactive nature of Lean — you select tactics based on the compiler’s feedback at each step. The rest of this post is about how much of it a machine can take over — and how.

Yes, Lean has its own biography.

informal vs formal reasoning

Let’s start with “how much.” A system can take over the entire loop, compiler feedback included — I’ll call this formal reasoning, following GasStationManager’s distinction: the system has access to a formal verifier, such as Lean’s compiler, and uses that step-by-step feedback as it works, the same way the human above did.

Or a system can take over none of that loop — reasoning its way to a full natural-language argument with no compiler checking any step along the way. That’s informal reasoning: the argument either holds up or it doesn’t, and nothing inside the loop tells it which.

That’s one axis. The “and how” is a separate question — what the system is built on: a specialized prover model trained on formal mathematics, a general-purpose model wrapped in agentic scaffolding, or a general-purpose model working on its own.

With both axes in hand, we can place the systems discussed below:

† “Informal” describes a stage, not the whole system — a system can reason informally and still use Lean elsewhere as verifier. What makes a stage informal is that its output isn’t checked by the verifier; it acts as a planner (a proof strategy, lemma, or subgoal) for a later stage to formally verify.

formal reasoning as search without informal reasoning

AlphaProof, jul2024¹

In July 2024, Google DeepMind announced that AlphaProof, a reinforcement-learning (RL) system. At high-level, it has three components:

• proof network: a 3B transformer model, pretrained on 300B tokens of code and mathematical text, then supervised fine-tuned on approximately 300,000 state–tactic pairs from Mathlib², a community-maintained library of formalized mathematics.
• actors: distributed workers who run Monte Carlo Tree Search (MCTS), which explore the space of tactics at each state under the network’s guidance.
• learner: updates the proof network from what the actors find, only active in training.

This design is inspired by AlphaZero, DeepMind’s agent family that first demonstrated superhuman performance in Go — but this time, the loop trains a model to prove, not to play. It’s not obvious that loop transfers, though: board games have a fixed set of legal moves and a simple rule for declaring a winner; theorem proving has neither of them. Before applying any AlphaZero-style method, therefore, proving has to be made to look like a game.

But if you recall how interactive proving works in Lean, you’ll find it is quite similar to a game: state is the position; choosing a tactic is making a move; and the no-goals state is the terminal condition — though unlike Go’s fixed move list, a tactic can reach into an ever-growing library of lemmas. Still, it’s enough to define the four elements of RL:

• the state, proof state.
• the action, tactic. Lean executes it and yields a new state.
• the reward, −1 per action applied.
• the return, the sum of rewards to termination.

Another challenge is where the training problems come from. In Go, AlphaZero can generate an endless supply of games just by playing against itself. Theorem proving doesn’t have this luxury: AlphaProof can attempt a proof and learn from whether it succeeds, but it can’t invent the theorem to attempt in the first place. Therefore, a specialized Gemini 1.5 Pro was employed to auto-formalize roughly a million natural-language problems into some 80 million Lean statements, and those serve as the problems the actors train on.³.

An actor is assigned a statement and a compute budget, and is asked at random to either prove or disprove it — many statements are false, as the autoformalizer guarantees neither faithfulness nor truth. The actor then sends the proof state, serialized as text like n : ℕ ⊢ ∃ p, n ≤ p ∧ Prime p to the proof network, which returns two things:

• A value: estimating the expected return G_t — where the search should keep spending effort.
• A policy: suggesting promising tactics to apply next, such as let p := minFac (n ! + 1) and by_contra! h — what the search should try.

Actors use these two outputs to conduct MCTS that executes sequences of tactics and evaluates their consequences. Picture a tree whose nodes are Lean tactic states⁴, edges are tactics. Each search iteration involves three phases:

• Selection: actors descend to a promising leaf, guided by the value together with the policy’s prior⁵ — the standard rule for trading off between what looks good and what has not been tried.
• Expansion: actors expand that leaf by sampling tactics (from the policy), check each one in Lean, discard the invalid ones.
• Backpropagation: the proof network estimates the new leaf’s value, which is sent back up the path so later rounds choose better.

When a problem resists both the network and a large search budget, AlphaProof uses test-time training. It generates a family of related statements around it — variations, weakened forms, special cases — and runs the same RL loop on them. The easier ones are provable where the original is not, so the loop gets reward where it would otherwise get silence, and the network arrives back at the original problem with trained techniques.⁶

DeepSeek-Prover-V1.5, aug2024

AlphaProof turned proving into a search problem, and solved three of the six problems from that year’s International Mathematical Olympiad⁷. The obvious direction for improvement is search efficiency — the space of possible proof paths is enormous.

The DeepSeek team, who had been working the same problem since May 2024 with DeepSeek-Prover-V1, raised a harder question: is the model actually planning a proof like human, or just searching — trying tactics, reading Lean’s verdict, trying again? They observed that the model behaves differently depending on what it is shown: in natural language, it generates detailed deduction steps; in Lean, it often relies on tactics to brute-force solutions. These tactics hide both the argument behind them and their likely outcome., making it harder for the model to learn how to decompose a complex proof goal.

V1.5, released that August, introduced two changes that work together. First, during supervised fine-tuning, the team supplemented formalized proofs with chain-of-thought material: a complete natural-language solution, and natural-language steps annotating the corresponding Lean tactics.

Second is the truncate-and-resume mechanism, which changes what a search step is in MCTS. Recall expansion: growing a leaf by proposing a move and checking it in Lean. AlphaProof’s version of that move is a single tactic — the network proposes one, Lean checks it, and the tree grows by a single step.

For DeepSeek-Prover-V1.5 instead of proposing a tactic at each expansion, the model generates a whole proof continuing from that node’s proof state to the end. Lean checks it, truncates at the first error, and parses whatever compiled into a chain of tactics, each one an edge to a new state beneath the node it expanded. A later expansion can then pick up from any node in that chain and generate onward. The model plans a stretch of reasoning at a time rather than a move at a time.

formal reasoning as programming/search + informal, non-rigorous

DeepSeek found that tactics alone didn’t teach the model to decompose a hard goal, so they augmented training and prompting with chain-of-thought material. The next step is to have the model generate that reasoning itself., or to be more specific, to plan a proof.

This is where the guessing lives. Nothing here is proved. The model does what a mathematician does at a whiteboard: tries a few small cases, notices a pattern, bets that some lemma is both true and useful, decides what order to attack things in. The output is a proposal, not an argument, and it can be wrong.

What that proposal looks like varies. It might be a paragraph of English, a list of named lemmas, or Lean code itself. The last one is the one to watch, because Lean code that compiles looks verified, and here it isn’t. A skeleton with its subgoals left open compiles fine — what Lean confirms is that the pieces fit together, that closing them would close the theorem. Whether any of them can be closed, or is even true, is exactly what the compiler was told to skip. Rigor only arrives once those gaps are filled.

DeepSeek-Prover-V2, jul2025

In July 2025, the DeepSeek team announced DeepSeek-Prover-V2, a prover model built on Draft, Sketch, and Prove⁸. First proposed in 2022, the framework takes an informal statement and:

• draft informal proof, by a human or a language model.
• generate formal proof sketch, which is a partial proof that outlines high-level conjectures and lemmas⁹
• prove remaining conjectures using provers (non LLM at the time of publication)

The center of action in DSP is no longer tree search, but the informal proof: it decomposes a complex task up front, before any formal search begins. What happens inside the prove step for a single conjecture is a separate question; it could still run a tree search of its own, just scoped to one lemma instead of the whole statement.

When the DSP paper appeared in 2022, language models could not reliably draft useful informal proofs. As foundation models improved, particularly at chain-of-thought reasoning, their informal proofs became increasingly useful guides for proof construction.

For DeepSeek-Prover-V2, that foundation model is DeepSeek-V3, a Mixture-of-Experts (MoE) language model with 671B parameters. When presented with a formal statement, DeepSeek-V3 will first analyze the problem in natural language (draft), decompose the proof into smaller steps as subgoals, translate each step into a corresponding Lean formal statement (sketch). After decomposition, the code consists of a sequence of have statements, each concluded with a sorry placeholder marking a subgoal to be solved. Each have becomes its own, independent Lean theorem-proving task, handed to a separate 7B prover model trained specifically for this: given the subgoal, it generates a complete formal proof for it in one pass — no tree, no expansion, just a direct answer to one self-contained problem.

The tasks aren’t fully isolated, though: solving them in order lets each one borrow from what came before. A subgoal’s statement is substituted in for the original goal, and every subgoal already proved earlier becomes an available premise — a lemma settled at step three is just there, ready to use, by the time the model reaches step five.

Seed Prover, aug2025

In 2025, two teams took on IMO with fully formal solutions. ByteDance’s Seed-Prover competed by official invitation under the committee’s July 18 deadline, fully solving four problems and partially solving a fifth — an officially recognized silver medal. Harmonic — a Sequoia-backed mathematics AI company founded by Tudor Achim and Vlad Tenev, the latter better known for Robinhood — reported their prover model Aristotle solved five out siex, which it describes as gold-medal-equivalent.

The Aristotle paper calls the resemblance between the two systems convergent evolution, and the list is long enough to justify the phrase. Both wrap informal reasoning around formal feedback. Both decompose a hard theorem into named lemmas, track which succeeded, and feed proved lemmas back as context for what remains. Both built separate geometry engines. Two teams arriving independently at the same architecture says more about where the field has settled than either system does alone.

On the formal side, Seed-Prover is a whole-proof model, and squarely in the programming mode: it generates a complete Lean proof, reads the compiler’s complaints, writes a summary of what went wrong, and tries again.

Its distinctive piece is its conjecture pool. A proposer module takes the unsolved problem, optionally with lemmas already proved, and emits 10 to 50 candidate properties at a time — that a function might be injective, surjective, monotonic, periodic — repeated until a pool of several thousand accumulates. Each conjecture is then attacked, and the survivors move into a lemma pool, scored by proof rate, semantic relevance, and proof length; the authors note that lemmas which proved hard tend to be the ones that end up mattering. Hundreds of the top-ranked are handed back to finish the main theorem.

This is a different bet from DSP, which converges from the start — commits to a plan, then proves each piece of it. Here the system diverges first: it generates candidates without knowing which are needed, then converges by keeping only the ones that provably hold.

Aristotle, oct2025

Aristotle sits in the same category on the informal side and diverges on the formal one. It follows DSP more literally than either: it drafts an informal proof organized around named lemmas, formalizes them, then solves each one with its own MCTS¹⁰, guided one action at a time. An action in Aristotle is a fragment of Lean code — possibly one tactic, possibly a sequence of them.

That last step is what separates it from everything else in this section. Seed-Prover and DeepSeek-Prover-V2 both hand a subgoal to a language model that writes a proof of it; Aristotle hands the subgoal to a tree search. The search from the previous section hasn’t disappeared, in other words — it’s been demoted. It no longer attacks the theorem, only the lemmas that an informal stage decided were worth attacking, which is a much smaller thing to search.

General-purpose model with agentic scaffolding (also formal reasoning as programming/search + informal, non-rigorous)

The systems in the previous section rely on a prover model. As general-purpose models have improved at mathematical reasoning, that specialization has begun to look less necessary. What if we just take a frontier model—whose exposure to Mathlib we may not even know—and pair it with the Lean compiler and a text editor, wrap them in a loop. Will it work?

In May 2026 Google DeepMind published AlphaProof Nexus. At the core of Nexus is a Gemini 3.1 Pro, a general purpose model. The agent reasons over a Lean file with sorry, makes a few search-and-replace edits, compiles, reads the errors, and edits again. If it runs out of turns with the sorry still there, it writes itself a comment about what it learned and starts over from the current file. A handful of these run in parallel with no shared state, and the first to produce a proof stops the rest.

It works well enough to be pointed at open problems. Nexus resolved 9 of 353 open Erdős problems, proved 44 of 492 open conjectures from the OEIS, settled a fifteen-year-old question on Hilbert functions, and improved a bound in convex optimization — at a few hundred dollars of inference per problem. I will be discussing the general loop of this agentic scaffolding by using Nexus as example. Other teams working along this frontier include Math Inc., Axiomatic, Logical Intelligence, Logos Research, and Axiom.

AlphaProof Nexus: what the loop actually looks like

Unlike a prover model that operates on Lean proof states, the agentic scaffolding operates on proof sketches. A sketch is a Lean file containing a partial proof, together with its compilation status; it may contain sorry for unproved goals and comments recording earlier attempts. ![[alphaproof_nexus_three_level_nesting.svg]] To start the workflow, the user would have to supply a Lean file whose proof contains sorry, optionally accompanied by natural-language context and further domain knowledge encoded in Lean — background lemmas, definitions, or a partial skeleton. This is the seed sketch: the first entry in the population, and the starting point for every episode until better ones exist.

From this seed, the agent spawns prover subagents that execute independently, with no direct communication between them; the population database is their only shared channel. Each subagent runs a sequence of episodes until it succeeds or exhausts its budget.

An episode is one multi-turn LLM inference loop that takes a sketch in and produces a sketch out. At the start of each episode, the subagent picks up an existing sketch from the population and opens a stateful conversation with a Gemini 3.1 Pro instance. Within that session it reasons via chain-of-thought and has access to two tools: a structured search-and-replace operation, and an optional AlphaProof call that attempts a goal and returns a proof, a disproof, or failure. Tool results become context for the subsequent turn. After each edit, Lean is invoked to check whether the sketch compiles; if it does not, the error message is appended to the session and directs the next turn.

The episode ends when the session concludes — successfully, if the sketch compiles with no remaining sorry. If the sketch still contains sorry, the subagent first writes a comment into it summarizing what it learned: which approaches failed, which lemmas looked promising, which subgoal is the bottleneck. Either way, the resulting sketch is checked with SafeVerify¹¹, which confirms that the problem statement was not changed unsafely and that the proof genuinely compiles, guarding against environment exploits. Sketches that pass are admitted to the population.

When a validated, sorry-free sketch appears in the population, the agent outputs it as the final Lean proof.

Axiomatic’s Ax_Prover: Can it be simpler?

Axiomatic started where Nexus does. Ax-Prover, their agentic scaffolding, prescribed the proof procedure step by step — sketch the argument in natural language, formalize it into a chain of haves each ending in sorry, then walk them in order. It exposed the full Lean language server over MCP, and let the agent decide when to compile.

Their next system deleted nearly all of it, and works about as well.

The prescribed procedure is gone; now the proposer writes a whole proof, the compiler rejects it, and it writes another one, up to fifty times, regenerating the file each round rather than editing it.

The language server is gone, down to one Mathlib search plus web search, fired in a single round before the proposer commits; goal states still arrive, but as feedback the harness extracts at each sorry, not as something the agent can ask for.

In general the agent is given less discretion: before it could choose when to compile, now compilation happens at the end of every round regardless. The loop takes over orchestration, and the compiler takes over most of verification — checking for sorry, added axioms, suggestion tactics like apply?. That leaves the model doing two things: proposing proofs, and the one check a compiler can’t make, whether the agent quietly changed the theorem it was asked to prove. That last job is what SafeVerify does for Nexus, minus the formal guarantee.

Axiom’s AxiomProver: autoformalization

Axiom’s system, axiomprover, moves the boundary the other way. Its published account begins not with a Lean file but with a natural-language statement, a task description, a Lean version, and an incomplete proof containing correctable errors; AxiomProver formalized it itself, emitting the formal statements and the proof as separate files.

Pulling autoformalization inside the loop removes the human from the one step where the guarantee is anchored — a machine-checked proof of the wrong statement checks out fine — while also removing the bottleneck that makes formal methods expensive.

Recap: vibe mathing has come

Informal reasoning used to be a component of the prover model. With agentic scaffolding, it’s almost the entire system. Prover models dealt with tactics; agents deal with files. What’s left should look familiar to anyone who has watched an agent write software: a model in a loop with a compiler, editing a file through search-and-replace, keeping a scratchpad, and running its output past a reviewer. Theorem proving starts to look like vibe coding.

Another trend is the growing importance of autoformalization. A general-purpose model may or may not have been fine-tuned on Lean as a prover model has, so it often needs external help to work effectively with the formal language—for example, access to Mathlib through an LSP or MCP interface. The breadth of that library becomes a major bottleneck on its problem-solving capabilities. Mathlib contains roughly a quarter million formal declarations: already a great deal of mathematics, but still a rounding error beside the informal literature. Math Inc.’s OpenGauss is one agent built to help autoformalize theorems.

That gap matters beyond just solving more math — it bounds how far an agent’s reach can generalize across subjects. When Ax-Prover moves to quantum theory or cryptography, the proofs are not necessarily harder; Mathlib simply has no quantum mechanics. So before anything can be proved in a new domain, the domain has to be formalized first.

The tricky part is that formalization can’t fully be checked: you can verify a proof, but you can’t verify whether an autoformalized statement is faithful to what the mathematician meant. That gap will matter even more for formal verification, where the translation isn’t prose into Lean but code into Lean it claims to satisfy. That’s where this goes next.