Xena | Mathematicians learning Lean by doing.

Mathematicians learning Lean by doing.

Xena | Mathematicians learning Lean by doing. Xena Mathematicians learning Lean by doing. Skip to content Home About Xena Student projects Installing Lean and mathlib Bluesky Useful links. ← Older posts Human mathematicians are being outcounterexampled Posted on July 20, 2026 by xenaproject 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 con

related reading

• Mathematics in the Library of Babel - Daniel Littdaniellitt.com
• 2510.01346arxiv.org
• What's new | Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Taoterrytao.wordpress.com
• Mathematicians in the Age of AI1footnote 11footnote 1I am grateful to Johan Commelin, Sidharth Hariharan, Bryna Kra, Emily Riehl, and Akshay Venkatesh for comments, corrections, and suggestions.arxiv.org
• [2510.01346] Aristotle: IMO-level Automated Theorem Provingarxiv.org
• A recent experience with ChatGPT 5.5 Pro | Gowers's Webloggowers.wordpress.com
• Lean (proof assistant) - Wikipediaen.wikipedia.org
• 2310.10631arxiv.org
• Inside the Secret Meeting Where Mathematicians Struggled to Outsmart AI | Scientific Americanscientificamerican.com
• Computational Complexityblog.computationalcomplexity.org
• Shtetl-Optimized >> Blog Archive >> Dispatches from the possibly last days of human relevancescottaaronson.blog
• Solve math, solve everything. — Math, Inc.math.inc