GoKawiilThe same week that Claude finished formalizing the proof of Fermat’s Last Theorem in Lean, a paper landed in my inbox titled, The Spherical Hadwiger Theorem. The Spherical Hadwiger Conjecture, which has been open since about 1974, describes a niche-but-important piece of integral-geometric machinery. I’m not going to get into the details of the conjecture here; if you are interested you can see a discussion in my previous post where the theorem (then still a conjecture) greatly simplifies the proof of a little lemma of mine from grad school.
But to the point: this new preprint by Wang & Wu of Hunan University apparently proves the conjecture using AI assistance. The final section contains the disclaimer:
During the preparation of this manuscript, 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. The authors reviewed and verified all AI-assisted mathematical content and suggested changes, made all final mathematical and editorial decisions, and take full responsibility for the manuscript.
This disclaimer leaves open the possibility that Codex did a substantial portion of the work that, until very recently, required a research-level mathematician: developing proof details, finding and fixing gaps, and apparently writing the paper. Moreover, the work is very polished and readable (if you are a research mathematician in this field).
To be clear, I haven’t fully verified the proof; I worked through it with Claude Fable and it passes the sniff test, but fully digesting it will take a bit more energy than I have right now. None of this is a knock on Wang & Wu—this seems to be a great paper, and is worth digesting. They’ve even followed all the principles for AI use laid out in the Leiden Declaration.
A milestone, close to home#
For me, the proof of the Spherical Hadwiger Theorem hits home. I tried to prove it in grad school, and made a half-hearted attempt again with AI assistance earlier this year. It’s not a headline-grabbing theorem. That didn’t save it.
I shouldn’t have been surprised. When GPT-4 launched, OpenAI released a report on the potential labor impact of LLMs. The exposure of the work of mathematicians to disruptions from AI was the highest of any category they modeled; the whitepaper estimated that 100% of a mathematician’s job was exposed to LLMs, across three distinct labor models. Higher than writers, translators, artists, and graphic designers. The only difference is that it took a bit longer for mathematicians to begin to feel the pain.
It’s tempting, if somewhat arrogant, to claim that this delay in LLM dominance in mathematics arose because research-level mathematics is among the most challenging human endeavors. I suspect the delay owes as much to research mathematics having less economic value—and less training data—than these other creative domains.
Off to the conservatory?#
... continue reading