Products You May Like
Machines can now check, and increasingly write, proofs that code meets its specification. What no proof can show is that the specification captures what its authors intended.
In May 1979, Communications of the Association for Computing Machinery published “Social Processes and Proofs of Theorems and Programs,” an argument that formal verification of computer programs could never earn the kind of trust that proofs earn in mathematics. Richard De Millo, Richard Lipton and Alan Perlis reasoned by analogy with mathematics. Theorems do not become trustworthy because a proof exists, they wrote; they become trustworthy because a community reads them, doubts them, simplifies them, teaches them and eventually builds on them. Program verifications are long, mechanical and unreadable, and no comparable community would ever form around one. Trust was a social product, and verification had no society.
Nearly 50 years later, machines have overturned one half of that argument and sharpened the other. The distinction now sits at the heart of making AI-generated software safe.
What Machines Solved
The overturned half is the claim that nobody can check a proof nobody reads. A modern proof assistant reduces an argument to steps validated by a small trusted kernel, and the kernel does not skim, tire or defer to reputation. Lean, the open-source proof assistant whose Mathlib library holds nearly 290,000 machine-checked theorems, has carried this from a research curiosity to a working tool at the frontier of mathematics. On August 1, 2026, ten results in mathematics and theoretical computer science were released by OpenAI, produced with an internal model and each accompanied by a Lean 4 certificate containing no unproved steps. No mathematician needed to read those proofs line by line, but for the question of whether each step followed from the last, it no longer mattered. The certificates are public, so anyone can rerun that check.
This is the inflection that has drawn investors and philanthropists toward formal methods over the past two years. Among them is Chris Hsu, founder of Kilometre Capital and the family office Rocketeer Management, whose Infinitude Foundation supports work on AI safety. Proving code had always been expensive, which is why it stayed largely confined to critical systems like aircraft avionics and rail signaling; the original seL4 microkernel proof took about 20 person-years for some 8,700 lines of C. But the economics of verification have changed, as AI can now do in days or weeks formalization work that used to take experts years. In September 2026, Anthropic reported formalizing the proof of Fermat’s Last Theorem in Lean in 11 days, against a five-year plan for a human-led project.
What Proof Still Can’t Tell Us
But a second question from the 1979 ACM paper remains standing. A proof establishes that a formal statement follows from its premises, yet it says nothing about whether the formal statement means what its author intended to ask. This question of intent is particularly relevant in software, which is designed by humans to complete tasks, not just establish the validity of a formal statement. Brian Cantwell Smith sharpened the point in 1985: proving a program correct shows that it agrees with a formal model, never that the model matches the world.
Three layers are distinguished in a 2026 analysis of machine-checked mathematics by Maher Kallel and Mohamed El Louadi. Derivational validity is whether each step follows, and a kernel checks it. Representational fidelity is whether the formal statement, together with every definition it rests on, captures the intended question. Epistemic significance is whether the result matters. In their account, only the first is mechanizable, and making it effectively free does not remove verification work. Rather, it shifts the burden onto the layers that still depend on scarce expert attention.
In May, an OpenAI model disproved the Erdős unit distance conjecture, an 80-year-old question about how many pairs of dots on a page can be spaced exactly one unit apart. Erdős conjectured that the count could grow only barely faster than the number of dots; the model found configurations that beat that conjectured limit. Nine mathematicians outside OpenAI checked the counterexample by hand and published what they called a “short, digested, human-verified version” of it, and the result entered the literature within days.
In August, the 10 certified results appeared, and four weeks later one of them, a result on Connes’s rigidity conjecture, remained the subject of an unresolved dispute over whether its formalization meant what it claimed. The result checked by people was absorbed quickly; the result checked by machine stalled on the question the machine-checked proof itself cannot answer.
The Burden of Proof
The same analysis that pulled those three layers apart went on to measure them, using the August corpus. It sorted the released work into two piles. On one side sit the proofs: the long, formal derivations that a proof assistant’s kernel (the small, tireless checker from earlier) validates step by step, eliminating the need for humans to read the derivation line by line. On the other side sit the statements: the far shorter formal claims, and the definitions they rest on, that a person still has to read to confirm they ask the intended question.
The size gap is enormous. The proofs ran to 20.6 megabytes; the statements, to 55.6 kilobytes. That’s a ratio of 379 to 1. Nearly all of the material is machine-checked and needs no line-by-line human reading, but those statements introduced 218 bespoke definitions of their own, rather than drawing on Mathlib, the community-vetted library a reader could take on trust. The surface a human has to audit is tiny in volume but seemingly irreducibly expert in kind.
Software Has the Same Problem
This is not peculiar to mathematics. The seL4 microkernel, which its developers say offers “the world’s highest level of assurance for an operating system kernel,” has a proof chain running from an abstract specification down to its C code and, on some processor architectures, to the compiled binary. Its functional correctness claim is that the C code “behaves precisely as specified in the seL4 specification and nothing more.”
Note what that phrasing makes conditional. The project is candid about the consequence. Alongside its proofs it maintains tests for already-verified code, a category the team describes as “testing the specification.” Yet even this kernel, whose verified code has had no reported functional-correctness defects since 2009, still keeps a human check on whether its specification says what its authors meant.
The Remaining Human Problem
Hsu has argued that formal methods are among the most underinvested foundations of AI safety. His reading of the current moment is that the 1979 objection has narrowed rather than dissolved. Proving code was the expensive part, and it is getting cheaper fast. The harder problem now moves upstream: deciding what should be proved. Lean’s creator, Leonardo de Moura, makes a similar argument: as AI takes over implementation, “specification becomes the core engineering discipline.” A December 2025 white paper by Hsu proposing a Stanford University center for AI alignment and consciousness science is one place this argument appears in writing, with “Formal Verification & Safe Deployment” among its four proposed research areas.
Meanwhile, the computer scientist Andrea Asperti and colleagues argued in 2009 that the critique’s “gloomy predictions” had been “largely refuted” by proof-assistant progress, and that the likelier direction of travel is mathematics becoming more like programming rather than the reverse. There is also a structural reason for optimism. As more definitions migrate into community-vetted libraries, fewer bespoke ones need auditing, and the surface requiring expert judgment keeps shrinking. The same logic now has to reach software. Mathlib gave AI a vocabulary for advanced mathematics; code has no equivalent yet. Open-source projects such as CSLib, a Lean library for computer science modeled on Mathlib, aim to supply one, so that a reviewer checking a specification reads familiar, community-vetted definitions rather than 218 new ones, and anyone can recheck the proofs without having to trust whoever produced them.
Both readings can be right at once. Engineering can compress the audit surface. What remains unproven is whether it can manufacture the auditor.