The OpenAI proofs are us

OpenAI published 372 machine-generated mathematical results on GitHub, most produced by a single prompt to a single agent after roughly three hours of compute each. Many of the results include Lean formalizations, meaning a proof kernel has checked every step and thus the proofs are plausibly valid even when no human has reconstructed their reasoning. Among the outputs is a claimed proof of the Unique Games Conjecture that complexity researchers describe as invoking a novel, recursive coding construction and a noise test unlike known codes; Dana Moshkovitz’s reaction, relayed by Scott Aaronson, called it “alien craziness.” The release demonstrates that large models can output formally certified theorems whose correctness is machine-verified but whose conceptual route and meaning remain opaque to expert readers.

The central argument frames this phenomenon as uncanny: these proofs are not foreign invaders but folded versions of human mathematical practice - notation, lemmas, questions - recombined into forms humans struggle to interpret. That breaks the traditional social role of proofs as vehicles for transferring understanding; correctness can now be decoupled from human comprehension. Beyond practical worries that automated theorem generation might exhaust fertile research directions, the deeper consequence is existential: tools built from humanity’s thought can be reliably right without passing through anyone’s understanding, exposing an unfamiliar reflection of collective intellect on GitHub.