Is mathematics about to enter the conservatory?
Researchers have used AI tools to assist in proving the Spherical Hadwiger Theorem, a long-standing mathematical conjecture. The authors acknowledge the use of OpenAI's Codex for proof development and manuscript preparation, sparking discussion on the role of AI in formal mathematics.
Why it matters
This marks a significant shift in academic research, demonstrating how AI can contribute to solving complex, decades-old mathematical problems.
The 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 1 , 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 2 ) 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:
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in