What Happens When Formalization Becomes Cheap?

The hope was appealing: AI could do the creative work, while a rigorous formal system, such as Lean, checked it. A major obstacle was the cost of expressing everything precisely enough in Lean. Coding agents such as Codex and Claude Code are reducing that cost. They can now formalize major results like Fermat’s Last Theorem and build large software projects with specifications and correctness proofs in Lean.¹

That progress has made another question harder to ignore: once we have formalized a claim and proved it in Lean, how much of the original problem have we actually solved? Sometimes a great deal; sometimes the important problem remains largely unresolved. Cheaper formalization has made me pay more attention to the gap between what we can prove and what we need to trust.

Recent security incidents involving AI agents and the debate about pacing frontier AI development make formal verification look like an attractive part of the solution.² I agree that it could be. But my experience has made me more cautious about how much assurance we should expect from it.

I keep having this conversation with friends, collaborators, and students thinking about research topics. This blog is an attempt to explain how my beliefs changed over eight years. I still believe formalization has important uses, but my research interests are broadening beyond it. Some of these views are speculative. I have been wrong before and may be wrong again. I’d be happy to compare notes, even if we end up disagreeing.

What a formal guarantee tells us

The appeal of formalization is that we can check an AI’s work without having to trust the AI. Whether it gives us a mathematical proof or a piece of software, we can ask it to spell out its claims, assumptions, and reasoning in a form a computer can check.

Suppose we want a program that sorts a list of numbers. Its output should be in ascending order and contain exactly the same numbers, including repetitions. Those two requirements are its specification.

See the complete Lean example

This example uses the library’s merge sort implementation and existing proofs. Tested with Lean 4.27.0.

An AI can write the program and prove that it meets this specification. Lean checks the proof. The resulting guarantee covers every input list, including ones nobody thought to test. That is the attraction of formal verification: the guarantee depends on the checked argument, regardless of who—or what—wrote it.

Why formalization is getting cheaper

For years, the cost of formalization dominated my thinking. Early work focused on training neural models to produce formal proofs. Open tools and datasets, including our CoqGym and LeanDojo projects, helped researchers build specialized provers. One successful approach was to specialize existing language models through post-training on formal statements and proofs. Goedel-Prover (2025), for example, used generated and checked Lean proofs to train increasingly capable models.

Specialized systems demonstrated substantial mathematical capabilities. In 2024, Google DeepMind’s Lean-based AlphaProof, together with AlphaGeometry 2, reached silver-medal-level performance at the International Mathematical Olympiad (IMO). ByteDance’s Lean-based Seed-Prover reported the same medal level the following year. AI could find arguments requiring substantial mathematical insight and produce machine-checkable proofs in Lean.

More recently, general frontier models have taken the lead in large-scale Lean formalization, often through coding agents such as Codex and Claude Code.

They often substantially outperform models built specifically for theorem proving. In retrospect, this makes sense: frontier models have a higher reasoning ceiling, and Lean fluency cannot substitute for finding an argument. General coding agents can also navigate codebases, search documentation, test ideas, and coordinate changes across files. These skills matter when the task grows from an isolated theorem to a large mathematical development or software project.

General models can also acquire the same specialized skills. If we can construct useful domain training data, frontier labs can use it too, either directly or by training specialists and transferring their skills into a general model.³ Lean expertise can become one capability among many.⁴

The practical change is how much of a project can be delegated. Anthropic’s Fermat’s Last Theorem project illustrates the scale: Claude agents formalized an existing human proof largely autonomously in 11 days. In software, agents can develop implementations, specifications, and correctness proofs together across large codebases.

This is what I mean by formalization becoming cheap: much less specialist human labor, though compute and libraries still matter. For many tasks with a clear statement and a correct informal argument, so little specialist intervention is needed that I sometimes call proof search and parts of autoformalization effectively solved.

This is much of what I hoped for when I entered the field. But working on VeriTile changed my expectations of what cheaper proofs would let us guarantee.

What I learned from VeriTile

VeriTile, led by Zenan Li, uses Lean to verify GPU kernels: the small, performance-critical programs that do much of the numerical work in AI training. We started the project with a possible path to recursive self-improvement in mind: an AI could optimize its own kernels, prove its changes correct, and use the faster kernels to train the next model.

Why kernels looked so promising

Training a large model is expensive, so engineers reorganize computations to make better use of the GPU and save time throughout a run. But an error may stay hidden until training deteriorates much later. By then, finding the cause can be harder than fixing it. Every optimization therefore raises the same question: did we preserve the behavior we care about?

Kernels are relatively compact, and their intended computations appear mathematical. We can often write a slow, straightforward reference implementation, then ask whether a faster one does the same thing. Here it seemed we could specify exactly what “correct” meant and let AI do the optimization and proof work.

What we could prove

In VeriTile, kernels are written in a Triton-style language embedded in Lean, giving each operation a precise meaning. Agents can then prove that a kernel meets a specification or matches a reference, with Lean checking their work.

See how VeriTile represents a kernel

One example is FlashAttention, which makes the attention computation in language models more efficient. A straightforward implementation of attention creates a large array of scores; FlashAttention works through smaller blocks to avoid it. The code looks quite different from the formula it implements. VeriTile proves that FlashAttention computes the same function as a straightforward reference, using arithmetic over the real numbers.⁵ The proof covers all inputs satisfying its assumptions.

This rules out implementation mistakes that testing might miss. But would the faster kernel preserve training outcomes? That depends on what mathematical equivalence means for the actual computation.

When exact equivalence asks for too much

If a replacement preserves outputs down to the last bit and all other relevant behavior, training cannot tell the difference. Proving this bitwise equivalence in an accurate execution model would justify the replacement. Many useful optimizations, however, change how arithmetic is grouped. Floating-point arithmetic is not associative: rounding intermediate results means that changing the grouping can change the result.

This prints 1.0 0.0, although both expressions equal 2 in real arithmetic. In a GPU kernel, such regrouping can enable parallel execution. Demanding bitwise equivalence would rule out many useful optimizations. Different outputs need not harm training, but small differences are not always harmless. A better prover cannot prove a false statement. We need another claim, such as a bound on the numerical difference.

How small is small enough for training?

An error bound tells us how much the outputs can differ, but how much can training tolerate? Small differences can affect many later steps. We need to connect the kernel’s numerical behavior to the training outcome we want to protect, and that connection may depend on the data. There may be no useful worst-case guarantee across all datasets; we may need to know whether an optimization works on ours. For the systems and optimizations we cared about, machine learning theory did not give us a practically useful answer.

In practice, AI researchers compare training runs using optimized kernels against a slower trusted reference. These experiments are expensive and cannot guarantee the full-scale outcome, but they test the behavior we care about more directly. When confidence is insufficient, AI researchers may disable an optimization and accept slower training.

The self-improvement loop we imagined may still need expensive experiments before adopting an AI’s faster kernel, even after proving mathematical equivalence. This was the update for me: we knew what we wanted, but lacked a useful mathematical connection between the properties we could prove and the training outcome we cared about.

A missing specification is sometimes an unfinished document. But in this case, it can be a missing piece of science.

Better AI may help develop the missing theory. But that scientific progress does not follow simply from having a model that is very good at Lean.

The work before the proof

VeriTile exposed a gap between a clear goal and a useful mathematical claim. In other applications, the work starts even earlier: we have not settled what we want.

Consider smart contracts: programs on a blockchain that can control real money. Bugs can be expensive and difficult to fix after deployment. This looks like an excellent application for formal verification, and tools already exist for checking properties of these contracts. In practice, auditing draws on human review, static analysis, testing, fuzzing, and formal verification. Formal verification is often only a small part of that work.

Much of the work is figuring out what the client wants the system to do. Clients often do not know at the outset. Knowing that you want to protect users’ money does not tell you exactly what to prove. Arriving at a useful specification is a major part of the audit; cheaper proofs do not automatically resolve it. The sorting example started with this work already done: we knew what “correct” meant and could state it directly.

For a long time, the effort of writing formal statements and proofs dominated my thinking. AI is rapidly reducing that effort, making questions of intent and modeling harder to ignore. This is not a new observation, but I used to expect that making formalization easy would make these remaining problems manageable across a broad range of applications. I now expect them to determine where formalization delivers the most value.

AI can also help clarify a request, propose a model, or spot an omission. But we still need evidence that its choices are good.

A proof can establish that code meets an AI-generated specification without establishing that the specification captures what we want.

When is a proof worth it?

Part of the appeal of formal verification is the promise of closure: we have checked this, and we can move on. That peace of mind has real value. But in many applications, a proof settles only part of what we need to know. It covers every case under its stated assumptions; passing a collection of tests does not. Its practical benefit depends on whether it rules out failures that matter.

Like testing, fuzzing, code review, and experiments, formal verification needs to justify its cost.⁶ What could go wrong, and which approach gives us the most confidence for the effort involved? Sometimes a proof gives us enough evidence to adopt a change. In other cases, as with VeriTile, it rules out important errors but leaves us needing experiments to find out whether the change works as intended.

The strongest applications combine high stakes with a close connection between mathematical properties and practical requirements.

Hardware is a natural example: we can ask whether a circuit implements the intended arithmetic. Low-level systems software offers others: preserving program behavior through a compiler optimization, enforcing isolation in an OS kernel, or ensuring that a database transaction happens completely or not at all. Regulated industries may offer further opportunities where deployment depends on meeting precise requirements and providing evidence.

What about AI for mathematics?

Mathematics has an unusually direct connection to formal statements: the theorem itself is often what mathematicians care about. If a mathematical result matters to you intrinsically, establishing it rigorously has value in its own right.

Historically, AI researchers have also used mathematics to demonstrate what models can do. In 2025, an advanced version of Gemini Deep Think reached gold-medal-level performance with proofs written directly in natural language and officially graded by the IMO.

OpenAI’s Navier–Stokes work goes beyond contest mathematics. Its agents found the argument before a separate stage of Lean formalization and verification.⁷ Lean still had a useful role: checking the proof and giving others grounds to trust it.

If the whole pitch is “look, AI can do math,” I think that particular party is largely over.

A routine tool for coding agents

Falling costs broaden where verification is worthwhile: finding a few important bugs or proving one useful property can be enough. Jane Street’s recent change of view illustrates how cheaper proofs and more AI-generated code can change the economics. I expect formalization to become a routine part of coding-agent workflows, alongside testing.

Boris Cherny, the creator of Claude Code, recently reported that a few short prompts to Opus 5.5, using Lean, produced 16 pull requests fixing bugs and race conditions in the Claude Agent SDK. Those fixes are valuable even without a claim that the entire SDK is now correct. An agent might prove a property of one component and use property-based tests—checking a property on generated inputs—elsewhere. Complete verification need not be the destination of every project.

Can formal verification make AI safer?

In AI safety, recent security incidents make verified sandboxes an appealing idea: if an agent can find vulnerabilities that humans miss, perhaps we should put it behind boundaries that we can prove it cannot cross. I find this application compelling because a valid proof can rule out an entire class of attacks, under its assumptions. The attacker becoming smarter does not invalidate the theorem. We do not have to anticipate every attack to benefit from a guarantee that untrusted code cannot access protected memory.

For a particular deployment, two questions remain. Does the running system enforce the boundary? A proof about sandboxed code may rely on assumptions about the runtime and the underlying machine. Those assumptions need to hold in the deployed system. If another tool can retrieve the same data for the agent, the memory guarantee does not close that route.⁸

Are the restrictions sufficient for the task? Even a perfectly enforced boundary leaves the agent able to act within it. An agent that cannot read protected memory may still produce a harmful code change that a user then applies. That permitted channel needs other safeguards. Deciding which actions to allow, and what checks they require, brings us back to intent and the consequences of getting it wrong.

The debate about pacing frontier AI development makes these distinctions consequential. Verified safeguards could provide important evidence for deploying a more capable system. We still need to know which failures the proofs rule out, whether their assumptions hold, and what requires testing, monitoring, or other safeguards. “Formally verified” alone does not tell us whether it is safe to proceed.

What this changes for my research

As formalization gets cheaper, I expect it to be used more widely. My research is broadening toward the questions its guarantees leave open.

I am increasingly interested in how humans can justifiably trust AI’s outputs when a complete formal guarantee is out of reach.

Humans are weak, compute-limited verifiers: we may be unable to solve the same problems ourselves, and we cannot check everything an AI produces. I’m interested in approaches such as prover–verifier games: can we design interactions that help weaker verifiers distinguish correct reasoning from convincing mistakes? I am also interested in the institutions—rules, incentives, and accountability—that allow humans and AI agents to trust one another and cooperate while preserving meaningful human control.

The work I’m most excited about now connects verification with alignment and the design of systems in which humans and AI agents can reliably work together. My research agenda is still taking shape. Formalization will remain part of my work, and so will the habits it taught me: asking exactly what a claim says, what it assumes, and what would count as evidence for it. What has changed is how much I expect a formal guarantee to settle. I still want AI’s work to be trustworthy. I am less convinced that formalization alone will get us there.