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
- Automation Without Understandingarxiv.org
- A New Consciousness of Mathematicsapoorvapanidapu.substack.com
- unit-distance-remarks.pdfcdn.openai.com
- Xena | Mathematicians learning Lean by doing.xenaproject.wordpress.com
- The fall of the theorem economydavidbessis.substack.com
- Existential Risk from AI: An Exposition for Mathematiciansalkjash.github.io
- The AI math breakthroughs keep coming...youtube.com
- A Severe Misalignment of AI in Mathematicsterrytao.wordpress.com
- Look, Mom, I pressed a button!galoisrepresentations.org
- Formalizing Fermat's Last Theoremanthropic.com
- We need to talk about AI in mathematicsyoutube.com