The Proof Economists Skipped

Somewhere inside a quiet repository of formal proofs, a piece of software read a theorem that economists have been teaching for half a century — and refused to accept it. Not because the conclusion was wrong, but because a step was missing. An assumption had been stated, used, and built upon for fifty years, and no one had ever actually proved it. The machine noticed. That small, almost clerical flag may turn out to be one of the most consequential moments in the history of social science.

The software is part of EconLib, a project unveiled in June 2026 by Axiom Math — a company whose ambition is as audacious as it is simple: do for economic theory what the Lean community's Mathlib did for mathematics. Build a vast, public, machine-verifiable library of foundational results, in which every theorem is checked, step by step, by a proof assistant that cannot be persuaded, cannot be tired, and cannot wave its hands.

For mathematics, that revolution has been underway for years. For economics — a field that runs on theorems, equilibria, and existence proofs, but has never subjected its canon to mechanical verification — EconLib is something genuinely new. And its first major act was to find a hole.

What a Proof Assistant Actually Does

To understand why this matters, you have to understand what a system like Lean demands. A human mathematician writes a proof for other humans. That means shortcuts: "it is easy to see that," "by a standard argument," "the rest follows similarly." These phrases are social conventions — invitations to trust the author's judgment. They are also where errors hide.

A proof assistant accepts none of it. To get a theorem past Lean, you must spell out every inference in a formal language the computer can mechanically check against its axioms. There is no "clearly." There is no "the reader can verify." If a single logical link is absent, the proof does not compile. The machine does not grade on a curve.

This is why formal verification is such a powerful microscope. When you force a celebrated, decades-old argument through Lean, you are not asking whether experts believe it. You are asking whether it is, in the most literal sense, complete. And as EconLib's team discovered, "everyone has always believed it" and "it has actually been proved" are not the same statement.

The Hole in the Foundations

The result that made headlines involved a foundational theorem associated with the Nobel laureate Robert Aumann — a cornerstone of the kind of game theory and decision theory that underpins modern microeconomics. According to the reporting, Axiom's verifier flagged that Aumann had stated a structural assumption that he never fully proved. The argument worked, in the sense that generations of economists used it and built on it. But the underlying scaffolding — the part everyone took for granted — had never been formally established.

The unsettling part is the cascade. As Axiom's collaborators put it, almost every theorem built on top of that foundation was, in effect, resting on ground no one had examined. This is not an accusation of fraud or even of error; the conclusions may well be perfectly true. It is something subtler and more interesting: a discipline discovering that some of its bedrock was assumed rather than secured, and only finding out because a machine insisted on reading the fine print.

The project is being co-led, on the economics side, by Scott Duke Kominers, working with Axiom's team. Their framing is deliberately constructive: EconLib will be a public, open repository that other economists can contribute to, extend, and build upon — exactly the model that let Mathlib grow into a community-maintained edifice of verified mathematics. As of mid-June, the public repository already contained fourteen paper formalizations, eleven of them complete.

Why Economics, Why Now

Two forces converged to make this moment possible. The first is the maturation of AI-assisted theorem proving. Axiom Math has been building autonomous, multi-agent provers — ensembles of models that propose, critique, and assemble formal proofs in Lean, and that earlier in 2026 cracked previously unsolved mathematical problems outright. The same machinery that can search for a proof can be turned to auditing one, translating informal arguments into formal code and surfacing exactly where the translation breaks.

The second force is economics itself. Unlike many social sciences, theoretical economics is unusually mathematical — its results are theorems, its models are systems of equations, its claims about markets and incentives are often stated with the precision of geometry. That makes it the natural next frontier for formalization. If you can formalize a fixed-point theorem, you can formalize an equilibrium existence proof. The tools were ready, and economics was the field most shaped like mathematics.

From Mathlib to a Library of Markets

The template here is not theoretical — it has already transformed a neighboring discipline. Mathlib, the community-built library of formalized mathematics in Lean, grew over a decade from a handful of definitions into a sprawling, interdependent edifice containing hundreds of thousands of theorems, each one machine-checked and reusable. Its power is compounding: once a result is formalized, every future proof can build on it with total confidence, because the foundation is guaranteed rather than assumed. A young mathematician today can stand on a mountain of verified results without ever needing to re-check the rock beneath.

EconLib's wager is that economics can have the same thing — and that the field needs it more than mathematicians might expect. Economic theorems are not abstract curiosities; they shape antitrust enforcement, market design, auction rules, and policy that moves trillions of dollars. When the foundations of that theory carry unexamined assumptions, the stakes of the gap are not merely academic. The reporting on Axiom's first result deliberately framed it through antitrust and economic theory precisely because the formal scaffolding under those arguments is load-bearing in the real world. A library that certifies which results truly hold, and which merely seemed to, is infrastructure for an entire field's credibility.

What makes EconLib feel like a beginning rather than a one-off is that it is designed to grow the same way Mathlib did: publicly, collaboratively, additively. Each formalized paper becomes a brick others can build on, and each gap the verifier surfaces becomes an invitation — a clearly marked obligation that some economist, somewhere, can now step in and discharge. The audit is not a verdict handed down once. It is a living process that gets more thorough every time someone contributes.

What It Means to Trust a Field

It would be easy to read this as a story about a mistake. It is better understood as a story about epistemics — about how a discipline knows what it knows. For most of history, the verification of mathematical and economic knowledge has been a fundamentally social process: peer review, replication of reasoning, the slow accumulation of trust as more experts fail to find a flaw. That process is remarkably good. It is also, demonstrably, fallible in a specific way: it is bad at catching the things everyone assumes.

A formal library changes the substrate of trust. Once a theorem is in Lean and compiles, its correctness no longer depends on whether the right expert read it carefully on the right day. It depends on the axioms and the checker — a far smaller, far more auditable foundation. The promise of EconLib is that economic theory could become, brick by brick, a structure whose load-bearing claims are not merely believed but mechanically certified.

That shift has a curious psychological dimension, too. Mathematicians who have formalized their own published work often report the same humbling experience: the proof they were certain was airtight turns out to have a soft spot, a case they waved away, a lemma they assumed. Almost always the result survives — the gap is fillable, the theorem true. But the experience changes how you think about certainty. It replaces the warm confidence of consensus with the colder, more durable assurance of a checker that does not care how famous you are. EconLib is now offering economics that same uncomfortable, clarifying mirror.

There are honest objections. Formalization is laborious, and a library of fourteen papers is a seed, not a forest — much of economics resists tidy axiomatization, especially the empirical and behavioral work that does not reduce to theorems. Critics also warn that a verified proof guarantees only internal consistency, not real-world relevance: a model can be flawlessly correct and still describe a world that does not exist. And there is the deeper worry that prestige will flow to what is formalizable, quietly narrowing the field toward the kind of mathematics machines find tractable. These are real. But none of them undoes the central fact: a tool now exists that can read the canon and tell you, without deference, where the gaps are.

The Audit Has Only Begun

What happens when you run the rest of a discipline's foundations through the same machine? That is the question EconLib quietly poses. If a single pass over a celebrated theorem can surface a fifty-year-old gap, the obvious next step is to keep going — through the existence proofs, the welfare theorems, the equilibrium results that economics teaches as settled. Some will compile cleanly and emerge stronger for it. Others may reveal their own quiet "clearlys."

This is the strange gift of machine verification: it does not make human reasoning obsolete so much as hold up a mirror that never blinks. Economists are not being replaced; they are being given a collaborator that reads every line and trusts none of them on authority. The first thing that collaborator did was point at a wall everyone had leaned on and ask, politely and unanswerably, where exactly is the proof that this holds? For fifty years, no one had asked. Now something always will.