“They all sort of said, ‘Oh, well, that makes sense. Aumann knows this,’” Kominers told Fortune in a recent interview. The problem: Aumann never proved all of the underlying structures underneath. And almost every theorem built on top was resting on foundations no one had formally examined. Until now. Kominers said there was “something that was under the surface and people hadn’t noticed was relevant, and these structures were never taught … the proof was implicitly relying on more than people realized.”
That finding is the first public result of EconLib, a project Fortune can exclusively reveal that Axiom Math is building — and which its founders believe could reshape how economic theory is used in American law.
Hong joined my interview with Kominers and told me about a saying in the Lean community: “Every time a proof cannot be formalized, the proof is wrong.” When Axiom ran Aumann’s theorem through it, the debugger flagged something.
Instead, he rethought his assumptions about what AI actually was. “For most of my career, I never really understood what math actually is,” he said, pointing to his head. “I misunderstood math for having all of this information crammed in my brain.” Before, you needed years of training and practice to call yourself a mathematician, and others without a PhD just couldn’t. “I now realize that we’re at an era where knowledge has become cheap, but verification has become more expensive, by contrast. And also the value of creativity is much higher than ever before.”
That reframe is also, it turns out, the business thesis of the company he joined.
In December, the proprietary model AxiomProver achieved a perfect score on the Putnam Competition — the notoriously brutal math exam that has humbled Fields medalists. Only five humans have ever done the same. Hong was not one of them — a fact she raised herself, unprompted.
“AxiomProver scored three times more than my Putnam score,” Hong said, before offering what can only be described as mathematician humor: “We were joking in the office that we should have a ‘beat Carina party.’” She and Ono laughed. But they insist that AxiomProver and EconLib are no joke.
The idea, which Kominers is co-leading with Axiom’s team, is to do for economic theory what Lean’s Mathlib project has done for mathematics: build a formal, machine-verifiable library of foundational economic results. EconLib will be a public project, open for other economists to contribute to, extend and build on. At least one outside researcher has already asked to help build the library. EconLib is set to go live soon, Axiom told Fortune.
What excites Kominers about it is the kind of thing that sounds modest until you realize what it implies.”Economic theory is a century at least of ideas and methods and models,” he said. “We’re hoping to produce something that right out of the gate is useful to economists.”
“In formal economic antitrust analysis, there are often literally arguments about the foundations of the models used to derive the metrics written down in the merger guidelines,” Kominers said. “These are all economic theory models that deliver the statistics people use in the cases,” he said. “And my hope is that we can use these tools to put far more precision and clarity into what world model you’re assuming before you choose your metric.”
Also, Albrecht said the verification burden is real — the “hallucination” problem. Even as AI helps fill in the steps, Albrecht said there is “just no way around needing different people to approve and verify” new results — though “Lean helps get us a long way there.”
Since joining Axiom in March, Ono has started eight new papers and finished six using generative AI tools — many in fields he has never formally studied. He’s blown away by the company he’s keeping. “I’m writing a paper with Scott Kominers, one of the most famous mathematical economists in the world!” Ono said excitedly.
“There’s a huge missed opportunity in academia,” Kominers said, “where people are not thinking, or not enough people are thinking of the LLM as enabling them to scale their intellectual capabilities.” He said he lists his AI tools in acknowledgment footnotes — as collaborators, not minions — and is unapologetic about it. “It enables me to see beyond what I could see just myself, in the same way as talking with students and collaborators provides that same expansion of vision and expansion of scope.” He said he’s never been so productive in his entire life, calling it “surreal.”
In his papers, Kominers lists AI tools in detailed acknowledgment footnotes, saying that he thinks of them as collaborators. These acknowledgments typically give specific details about how the tool was used, including directly crediting them for methods and discoveries where appropriate.
Kominers cited advice that he gives to students: when you’re an expert in a field, you go through moments of discovering that you don’t know anything. Every two to three years, he returns to the foundational texts of matching theory — his primary specialty — and teaches it to himself from scratch, and comes away with a deeper understanding, yielding new papers and ideas. “This project,” he said of EconLib, “is like that for all of economic theory. I’m realizing I didn’t understand any of it. I have to reorganize it in my brain, rediscover all of the ideas.”
He looked almost embarrassed by how excited this made him. “It’s what people don’t normally talk about, like discovering that you know nothing as a superpower, but to me it is.”
Albrecht landed in almost exactly the same place. AI has turned him, he said, “a little bit more into a mathematician” — letting him formalize things he couldn’t pin down before because he lacked the pure-math training of a PhD. “That’s one more mathematician out in the world solving problems,” he said. “In a lot of ways it’s an exciting time.”
[This report has been updated with additional context from Scott Kominers on the implications of this breakthrough.]
