To cheer you up in difficult times 27: A major recent “Lean” proof verification

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.” (See Lean’s homepage and see here for an introduction to lean.)

Kevin Buzzard’s blog XENA is largely devoted to lean. “The Xena project is an attempt to show young mathematicians that essentially all of the questions which show up in their undergraduate courses in pure mathematics can be turned into levels of a computer game called Lean.” (Perhaps this could also appeal to old mathematicians especially those interested in computer games 🙂 .)

Six months ago Peter Scholze proposed over XENA a project of verifying using Lean a certain involved proof he had (and was not even sure about), a few weeks ago he reported on an amazing progress that was achieved. This is great news! (I thank Tammy Ziegler for telling me about it.) For more on Lean see this Quanta Magazine article by Kevin Hartnett, and this GLL post. As a form of celebration, I posted an MO question on experimental mathematics (that renewed my older MO question).


Kevin Buzzard and Peter Scholze

This entry was posted in Algebra, Updates, What is Mathematics and tagged , , . Bookmark the permalink.

4 Responses to To cheer you up in difficult times 27: A major recent “Lean” proof verification

  1. Pingback: Computer assisted verification of contemporary mathematics – SPP 2026

  2. Does that mean FLT can be formally verified “easily” as well?

    • xenaproject says:

      FLT will take some work! What can “easily” be done now is the beginning of the process, where one starts to formalise statements such as the Langlands-Tunnell theorem, Mazur’s theorem on torsion points, Ribet’s theorem, the Shimura-Taniyama-Weil conjecture, an R=T theorem etc etc and starts to prove theorems saying how all these things are related. Occasionally one will run into things which need a lot of technology, for example Langlands-Tunnell needs all the machinery of the trace formula for (non-compact) GL_2, and Ribet’s theorem needs all the machinery of the reduction of modular curves (and in particular a bunch of algebraic geometry) but certainly proving things like R=T at minimal level (the Taylor-Wiles theorem) looks accessible to me (a lot of the work will be making definitions). The full proof uses so much stuff though.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s