The Curious Engineer

All blogs / Math

Xena

xenaproject.wordpress.com

Mathematicians learning Lean by doing.

MathFunctional / PL theoryAI / ML

’17’18’19’20’21’22’23’24’25’26
Posts
121 from 22 Sep 2017 to 16 Oct 2026
Posting
monthly (8 in the last year)
Kind
community
Feed
https://xenaproject.wordpress.com/feed/

2026 7

  1. How to Formalize All of Mathematics
  2. To grieve, or not to grieve?
  3. FLT: Anthropic has beaten me to it
  4. The Annals Challenge
  5. Human mathematicians are being outcounterexampled
  6. Formalizing Fermat workshop
  7. Accelerating mathematics

2025 6

  1. Formalization of Erdős problems
  2. Formal or not formal? That is the question in AI for theorem proving.
  3. AI at IMO 2025: a round-up
  4. Think of a number: an update
  5. What is a quotient?
  6. Think of a number.

2024 3

  1. Can AI do maths yet? Thoughts from a mathematician.
  2. Fermat’s Last Theorem — how it’s going
  3. Lean in 2024

2023 2

  1. Formalising modern research mathematics in real time
  2. Lean 2022 round-up

2022 4

  1. Beyond the Liquid Tensor Experiment
  2. The Future of Interactive Theorem Proving?
  3. Teaching formalisation to mathematics undergraduates
  4. 2022 Xena Project undergraduate workshop

2021 17

  1. New year, new teaching material
  2. 2021 Xena Summer Projects
  3. Half a year of the Liquid Tensor Experiment: Amazing developments
  4. The trace of an endomorphism (without picking a basis)
  5. Induction on equality
  6. Induction, and inductive types.
  7. Formalising Mathematics : workshop 8 — group cohomology
  8. Formalising Mathematics : workshop 7 — quotients
  9. Formalising Mathematics : workshop 6 — limits
  10. Formalising Mathematics : workshop 5 — filters
  11. Formalising Mathematics : workshop 4 — topology
  12. Formalising mathematics : workshop 3 — sequences and limits
  13. Formalising mathematics : Workshop 2 — groups and subgroups
  14. Formalising mathematics : workshop 1 — logic, sets, functions, relations
  15. Formalising mathematics: an introduction.
  16. Lean Together 2021
  17. The end of the summer.

2020 18

  1. Liquid tensor experiment
  2. Thoughts on the Pythagorean theorem
  3. Two types of universe for two types of mathematician
  4. Lean for the Curious Mathematician 2020
  5. Division by zero in type theory: a FAQ
  6. Equality, specifications, and implementations
  7. Teaching dependent type theory to 4 year olds via mathematics
  8. Mathematics in type theory.
  9. The Sphere Eversion Project
  10. The complex number game
  11. Xena Project Thursday meetings start with talk tomorrow 21st May
  12. Summer projects 2020
  13. The invisible map
  14. No errors.
  15. Where is the fashionable mathematics?
  16. Lean is better for proper maths than all the other theorem provers
  17. My algebraic geometry course
  18. Lean Together 2020

2019 24

  1. Lean has real manifolds!
  2. Rigorous mathematics
  3. My visit to Microsoft Research
  4. Prove a theorem. Write a function.
  5. The natural number game — an update
  6. Counting binary relations: an apology
  7. Chalkdust, and the natural number game!
  8. Does anyone “know” a proof of Fermat’s Last Theorem?
  9. IMO 2019 Q1
  10. Lean does not (yet) have real manifolds.
  11. A computer-generated proof that nobody understands
  12. What is homotopy type theory? An amateur speaks.
  13. Proofs are not programs
  14. The inverse of a bijection.
  15. Equality part 3: canonical isomorphism.
  16. Equality part 2: syntactic equality
  17. Equality part 1: definitional equality.
  18. Perfectoid spaces!
  19. M1F, Imperial undergraduates, and Lean
  20. Happy pi day
  21. 2+2=4
  22. Lean in LaTeX
  23. A word on BIDMAS
  24. Column addition

2018 23

  1. Learning Lean by example
  2. Blue-eyed islanders (guest post)
  3. Maths undergraduate example sheets
  4. What is the Xena Project?
  5. Formalising mathematics — a mathematician’s personal viewpoint.
  6. Happy birthday Xena!
  7. What is a uniform space? How some computer scientists think about completions.
  8. What is a filter? How some computer scientists think about limits.
  9. 617 is prime
  10. Quadratic Reciprocity and (p^2-1)/8
  11. Summer project
  12. (a+b)^3
  13. Tonbridge
  14. Function composition
  15. Group Theory revision
  16. Proofs by induction
  17. No confusion over no_confusion
  18. Mini-tutorial : Currying.
  19. Schemes!
  20. Working with integers
  21. Recent student successes
  22. What maths is already in Lean?
  23. Complex numbers! And M1F theorems.

2017 17

  1. How to install mathlib and keep it up to date
  2. Which definitions do we want in our library?
  3. Complex numbers? Intermediate Value Theorem?
  4. Sessions moved to Mondays in weeks 7 and 8
  5. Building the non-negative integers from scratch
  6. Rational powers
  7. How is Xena doing?
  8. Types
  9. Jeremy Avigad’s Logic and Proof course
  10. Sheet 1 Q2,Q3
  11. More easy Lean proofs [difficulty : quite easy]
  12. Note for Imperial undergraduates
  13. What Xena is not.
  14. First question done!
  15. Proving trivial things with Lean [difficulty : quite easy]
  16. Installing Lean (and VSCode) on Windows from scratch
  17. How far can a computer get on the maths degree at Imperial College?