Gamburd warns OpenAI's unread Lean proof is a Hobbesian bargain

Mathematician Alexander Gamburd has filed an essay on arxiv about OpenAI's recently announced Lean proof: 166 pages, 616,000 lines, produced in 88 hours by some 10,000 software agents, and read in full by no human being at the time of writing.

"A proof has historically been two things: a certificate that a theorem is true, and a demonstration that lets another person see why," Gamburd writes. "OpenAI delivered the first without the second."

The judgment pivots on the next move. "What matters is not what the Silicon Leviathan (OpenAI and its peer competitors) produces but rather what we accept," the abstract argues. Accepting the certificate without the demonstration, Gamburd writes, is "the Hobbesian bargain: authority, not truth, makes the law." Borrowing from Panofsky, he calls the result "a Middle Ages in reverse," its new authority a "subhuman superintelligence." The German coinage in his title, Aufklärungsdämmerung, is the twilight he thinks the Enlightenment is in.

The abstract names no specific theorem and no mathematician who has tried to read the file. It names only a demand: "that nothing counts as mathematics until a human being has understood it." Two of the researchers we follow were circulating the piece in the days after it first posted.