"Is mathematics about to enter the conservatory?" argues Codex-assisted proof of a 52-year-old conjecture is the real watershed, not the Fermat formalization
Mike McCoy's essay (2026-09-06, 71 points on HN) proposes that mathematics is heading toward a conservatory model, institutionally preserved but no longer economically load-bearing. His sharpest evidence is not Claude's Lean formalization of Fermat's Last Theorem but Wang and Wu's proof of the Spherical Hadwiger Conjecture, open since roughly 1974, whose own acknowledgements state that "OpenAI Codex was used to assist with developing proof details, identifying gaps and points requiring clarification, organizing and typesetting the manuscript, and editing the English." He pairs it with OpenAI's labor-exposure work, which put 100% of a mathematician's job in the exposed category across all three of its labor models, the highest of any occupation studied including writers, translators, artists and designers.
Source
↳ Follow the thread