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

• Human mathematicians are being outcounterexampledxenaproject.wordpress.com
• The fall of the theorem economydavidbessis.substack.com
• Can AI do maths yet? Thoughts from a mathematician. | Xenaxenaproject.wordpress.com
• Formalizing Fermat's Last Theoremanthropic.com
• Existential Risk from AI: An Exposition for Mathematiciansalkjash.github.io
• Mathematics in the Library of Babel - Daniel Littdaniellitt.com
• The AI math breakthroughs keep coming...youtube.com
• A New Consciousness of Mathematicsapoorvapanidapu.substack.com
• A Severe Misalignment of AI in Mathematicsterrytao.wordpress.com
• FLT: Anthropic has beaten me to itxenaproject.wordpress.com
• Declaration — Math and AImathandai.org
• What sort of maths are LLMs good at?gowers.wordpress.com