Human mathematicians are being outcounterexampled | Xena
It’s been an interesting few weeks for counterexamples. This post is basically my perspective of what has been going on in the world of formalization, AI tools and, in particular, counterexam…
It’s been an interesting few weeks for counterexamples. This post is basically my perspective of what has been going on in the world of formalization, AI tools and, in particular, counterexamples. Unit distance Two months ago today (20th May 2026), ChatGPT disproved Erdős’ Unit Distance conjecture in discrete geometry. This is now old news but I had to start somewhere. The announcement was accompanied with testimonies by human mathematicians, many of whom I knew and a few of whom I trusted, saying that they believed the argument (they had been given early access to it and had checked it).…
saved by
related reading
- What Happens When the World is Run on Code No One Understands?time.com
- unit-distance-remarks.pdfcdn.openai.com
- An OpenAI model has disproved a central conjecture in discrete geometry | OpenAIopenai.com
- Xena | Mathematicians learning Lean by doing.xenaproject.wordpress.com
- A New Consciousness of Mathematicsapoorvapanidapu.substack.com
- Formalizing Fermat's Last Theoremanthropic.com
- The fall of the theorem economydavidbessis.substack.com
- Mathematics in the Library of Babel - Daniel Littdaniellitt.com
- FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- Shtetl-Optimized >> Blog Archive >> Dispatches from the possibly last days of human relevancescottaaronson.blog
- What's new | Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Taoterrytao.wordpress.com
- A recent experience with ChatGPT 5.5 Pro | Gowers's Webloggowers.wordpress.com