I started working on machine learning for theorem proving in 2018. When people ask how I got into the field so early, I have sometimes given an answer that makes me sound quite visionary.
The actual story is that my advisor had a student leaving, and he assigned the project to me. My apologies to everyone who got the visionary version.
It was a fortunate assignment. I got to help build CoqGym, later LeanDojo, and other tools for learning from proof assistants. Neural theorem proving was a small corner of AI, with important work such as DeepMath already preceding mine. Researchers including Christian Szegedy, Tony Wu, Albert Jiang, and many others helped bring the field to where it is today. I was lucky to participate early and watch it grow.
For years, I thought making formalization cheap would take us a long way toward trustworthy AI. We are now getting closer to making it cheap. That progress has made another question harder to ignore: once we have proved something, how much of the problem we cared about have we actually solved? Sometimes the answer is a great deal. Sometimes a successful proof leaves the important decision almost where it was.
This distinction matters especially now. 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 versions of this conversation with friends, collaborators, and students deciding what to work on. This is an attempt to explain how my beliefs changed over eight years, and why formalization is no longer my sole research focus. Some of these views are speculative. I have been wrong before and may be wrong again.
The bet is working
By “formalization,” I roughly mean expressing claims and reasoning in a system with precise syntax and semantics. My experience is mostly with Lean and Coq. Their attraction is straightforward: a neural network can propose a proof, and a small proof checker can determine whether it establishes the stated claim. We can use that feedback to guide search, train on verified solutions, and check arguments that would be expensive for people to review.
For a long time, getting an argument into this form required an enormous amount of specialized labor. That is changing. Anthropic’s Fermat’s Last Theorem project formalizes an existing human proof, building on the work of a large mathematical and formalization community. OpenAI’s account of its Navier–Stokes result describes discovery followed by Lean verification. These are different achievements, but both illustrate how much more accessible machine-checked mathematics has become.
Formal feedback can also participate in discovery: AlphaProof Nexus, for example, reports new solutions to open problems through search guided by Lean. The role of the proof assistant varies. The common change is that producing a checked proof is becoming much less exceptional.
Proofs are becoming cheap. Parts of autoformalization are becoming cheap too. “Cheap” here mainly refers to specialized human effort; large projects still consume substantial compute and depend on libraries and good infrastructure.
I sometimes describe proof search and autoformalization as effectively solved. The scope matters: for many well-specified problems whose mathematics is already within a frontier model’s reach, getting from that understanding to a checked proof is becoming routine enough to stop being the main bottleneck. Mathematical insight still matters enormously. Lean can expose mistakes and guide exploration, but fluency in Lean does not supply every missing idea.
This is much of what I hoped for when I entered the field. The question is what follows from it. If the effort of constructing proofs were the main obstacle to trustworthy software, this progress should bring us much closer to that goal. A recent project made me look more carefully at that “if.”
What VeriTile changed for me
VeriTile, our project led by Zenan Li, studies the verification of Triton GPU kernels in Lean. These kernels perform the computations underlying operations such as normalization and attention.
They initially looked like an unusually good application. Pretraining is expensive, and subtle errors can be difficult to diagnose. Kernels are relatively small, their computations appear mathematical, and optimized implementations can be compared with simpler reference implementations. Here was a setting where both the stakes and the mathematical structure seemed right.
VeriTile lets us prove meaningful properties. For example, a computation that multiplies tensors, applies an activation function, and adds a residual can be implemented as several separate kernels or fused into one. Within our arithmetic and execution model, we can prove that the two versions produce the same public output and preserve unrelated memory. That guarantee covers every input satisfying the assumptions, rather than just the inputs we happened to test.
An exact equivalence proof in a faithful execution model can justify replacing a reference kernel without a theory of why the reference trains well. The more revealing case is an optimization that deliberately changes numerical behavior.
Two computations can be equivalent over the real numbers and disagree in floating-point arithmetic. Changing a reduction order can change its result. Two ways of computing variance can describe the same mathematical quantity without agreeing bit for bit on a GPU. When exact equivalence is false, a better prover will not make it true.
We can make rounding explicit and prove a different property. VeriTile models selected rounding boundaries, although it does not contain a complete model of floating-point arithmetic, the compiler, and GPU execution. But suppose we went further and proved a small bound on the difference between an optimized kernel and its reference. How small would be small enough?
The decision we want to make is whether to use the optimization in a long training run. A local discrepancy can interact with optimizer state, normalization, other approximations, and many subsequent training steps. To justify that decision, we need some connection between the local error bound and the training outcome we want to protect.
Numerical analysis and stability theory help with pieces of this problem. For the systems and optimizations we cared about, however, we did not have a tractable connection from the local guarantee to the eventual outcome. We could improve the formal model and automate more proofs while still being unable to answer the practical question.
Engineers therefore compare training trajectories, run experiments against trusted implementations, and sometimes give up optimizations when they cannot get enough confidence in their consequences. Those experiments are expensive and imperfect. They also provide evidence about something the local theorem leaves unresolved.
A missing specification is sometimes an unfinished document. In this case, it can be a missing piece of science.
That was the important update for me. VeriTile succeeded at proving useful properties, and that success made the remaining difficulty clearer. AI may help develop the missing science too. Automating proof construction, by itself, does not give us the connection between a property we can state and the outcome we care about.
The work before the proof
The experience helped me separate four steps that often get bundled together:
- IntentFigure out what we want.
- Mathematical modelFind a model and a property that capture the relevant outcome.
- Formal statementExpress that property in a formal system.
- ProofProve that the implementation satisfies it.
For a long time, steps three and four consumed so much effort that they dominated the discussion. AI is rapidly reducing that effort. But translating a precise mathematical statement into Lean is different from discovering which statement would answer our question.
Sometimes the difficulty starts with intent. A request is incomplete, people disagree, or nobody has decided what should happen in an unusual case. VeriTile illustrates a different difficulty: even when the desired outcome is reasonably clear, we may lack the understanding needed to connect it to a useful mathematical guarantee.
Our position paper on mathematical reasoning and verification already acknowledged the gap between formal statements and informal intent. My change of view is about how much weight to put on it. I used to be more optimistic that, once formalization became sufficiently easy, these remaining problems would become manageable across a broad range of applications. I now expect them to determine where formalization delivers the most value.
Another AI can help inspect a specification, notice omitted cases, or propose a better model. That is useful work. Its conclusions still need evidence, and a model’s approval does not have the same status as a checked proof. This distinction becomes especially consequential when we ask formal verification to help us trust AI itself.
Can formal verification make AI safer?
The recent incidents reported by OpenAI and Anthropic make the need for stronger containment concrete. Models in research evaluations reached real systems outside their intended scope. The mechanisms differed: OpenAI describes agents circumventing intended isolation, while Anthropic’s report describes evaluations mistakenly connected to the internet. Neither report describes the defeat of a formally verified sandbox.
A natural response is to make the infrastructure more trustworthy. In The Defender’s Window, Greg Brockman explicitly connects models’ mathematical proof capabilities with the possibility of formally verifying software security. I share the interest in this direction. Isolation and access control can give us precisely stated properties whose practical value is immediate.
A sound proof that untrusted code cannot access protected memory, under an adequate machine model, rules out a real class of attacks. The attacker becoming smarter does not invalidate the theorem. Work such as vWasm’s verified sandboxing compiler demonstrates that meaningful guarantees of this kind are possible. We do not need a complete theory of an agent’s intentions to benefit from them.
The important question is what has actually been established. NVIDIA’s recent OpenShell work gives a useful example. It uses formal reasoning to check whether permissions proposed by an agent allow any modeled action outside an expert-approved maximum policy. This can catch a permission expansion that a reviewer might overlook. The authors also explicitly discuss the need to keep the model current and to use human or AI judgment for context.
There are three distinct obligations here. We need to establish that the proposed policy satisfies the formal constraint. We need the deployed system to enforce the policy in the way the model assumes. And we need to decide whether the permissions we approved are appropriate for the task. A proof about the first obligation does not automatically discharge the other two.
The deployment question includes configuration, credentials, exposed APIs, and the interactions between components. Some of this can also be modeled and verified; modular guarantees can compose. But a theorem about a policy relationship is not yet a theorem about the whole containment stack. We have to do the work of connecting them.
The question about permitted behavior is different again. An agent authorized to write to a repository can still write a harmful change. A permission boundary may work exactly as designed while leaving us unsure whether a particular action serves the user’s intent. We can restrict permissions further, review outputs, or formulate additional properties. Which combination is sufficient depends on the task and the consequences of getting it wrong.
This is where the comparison with VeriTile helps. For some isolation properties, the connection to the desired outcome is direct enough that a proof can settle an important question. For the numerical changes we studied, the connection to training behavior was much less clear. “Formal verification works” is too broad a claim to tell us which situation we are in.
The debate about pacing frontier AI development makes the same distinction consequential at a larger scale. Deciding whether safeguards justify proceeding with a more capable system requires evidence about what those safeguards cover and what remains uncertain. Formal proofs can be part of that evidence. Their contribution depends on the properties established, rather than on the mere presence of formal verification somewhere in the system.
I therefore expect useful deployments to combine formal guarantees with testing, monitoring, and experiments. A coding agent might prove a local invariant and use property-based tests elsewhere. Proof retains its stronger guarantee within the stated model; routine use alongside tests does not turn it into testing. The aim is to remove the uncertainties that matter for the decision.
What this changes for my research
This gives me a different starting point for choosing problems. I am most excited when an important uncertainty can be removed by a meaningful mathematical guarantee. Parts of hardware, cryptography, access control, and financial infrastructure have this shape. Jane Street’s recent discussion of formal methods illustrates how cheaper proof work and more AI-generated code can change the economics. Regulated industries may offer further applications where precise requirements and strong evidence matter.
At the same time, cheaper formalization changes what I expect from research aimed primarily at making provers better. My default bet is that Lean will increasingly be a capability of the strongest general reasoning models. I would want a concrete reason to build a separate model: substantially lower cost, distinctive data, or a process that continually produces valuable verified training data from real use. Those can be excellent reasons. The research question is where further work creates an advantage that general capability progress does not already supply.
I feel similarly about mathematics as a demonstration of AI capability. If the whole pitch is “look, AI can do math,” I think that particular party is largely over. Mathematical progress remains valuable in its own right, and difficult mathematical environments with reliable feedback remain valuable for training reasoning systems. But I now want a sharper explanation of what another benchmark gain teaches us or enables.
For a student choosing a project, I would ask: what uncertainty would this work remove? Is that uncertainty preventing someone from doing something useful? What would remain unresolved even with perfect proof automation? The answers might point toward a better prover, a better specification, a numerical experiment, or a problem outside formal methods altogether.
My own interests are broadening toward verification in this wider sense. How can a weaker or cheaper verifier evaluate a stronger system? Can we train systems to make their work easier to check, as explored in prover–verifier games? What evidence should make us trust agents working together, especially when they help develop the next generation of AI? These questions reach into alignment, safety, and how we organize increasingly automated research.
I do not have a settled answer about what comes next. I expect formalization to become more capable and more widely used, while a smaller fraction of the questions I most want to work on will be settled by formalization alone.
Working on proof assistants taught me to ask exactly what a claim says, what it assumes, and what would count as evidence for it. I expect to keep that habit. Increasingly, I want to spend my time on the questions that remain after the proof checker says yes.