Scott Kominers has taught Robert Aumann’s 1976 theorem dozens of times. He’s assigned it in economics courses at Harvard. He’s built on it in his own research. So when Axiom Math’s formal verification system flagged a gap in the proof’s foundations earlier this year — an assumption Aumann stated but never actually proved — Kominers did what any rigorous economist would do. He called his colleagues.
“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.”