I'm super excited about this. Hope it gets moved to its own repo so it's easier to find and send to other people. I was always curious about math, and Tao's Analysis was the first textbook that really showed me how it can be constructed in a rigoruous way my programming brain was hoping for. Then I got a bit into Lean, and similarly it was very satisfying but Mathlib is a bit complicated to learn math concepts from. So it's nice to see a bridge from the book to the tool.
It's nice to see theorem proving gain some momentum in a mainstream mathematics topic such as analysis.
In PLT, we already had a flagship book (The Formal Semantics of Programming Languages by Winskel) formally verified (kind of, it's not a 1-to-1 transcription) using Isabelle (http://concrete-semantics.org) back in the mid 2010s, when tools began to be very polished.
IMHO, if someone is interested in theorem proving, that's a much simpler starting point. Theorems in analysis are already pretty hard on their own.
It will be incredibly interesting to assess how the mainstream "textbook" approach to the subject compares to the one taken in the Mathlib. In general, formalized math libraries make it comparatively easier to state results with a maximum degree of generality and to refactor proof developments for straightforwardness and elegance.
(Refactoring is of course made easier because the system will always keep track of what follows logically from what. You don't have that when working with pen and paper, so opportunities to rework things are very often neglected.)
It is a natural question also to ask whether it makes sense to teach the Mathlib, "maximum generality" version of real analysis, or at least something approaching that, in an academic course. Same for any other field of proof-based math, of course.
He also has is own YouTube channel with a few videos where he uses Lean [1]. I don't know much about any of it, but seeing him at work, with and without LLMs, was cool.
I think this is a very nice project and a very nice approach for a foundational topic such as analysis.
A couple immediate worries:
1. Core analysis results in Mathlib work with limits in a general, unified way using the notion of filters. There are nevertheless some ad-hoc specializations of these results to their epsilon-delta form. I presume that Tao's Analysis uses a more traditional epsilon-delta approach.
2. Mathlib moves fast and breaks things. Things get renamed and refactored all the time. Downstream repos needs continual maintenance.
I have a pretty radical opinion that math education should be focused on building Computer Algebra Systems like Mathematica and Theorem provers like Lean with a heavy focus on visualization and practical applications. Taken to the extreme this could mean never doing paper math while being able to prove everything you learned in Lean.
I feel our current system's focus on endless manual calculations that seem so useless is boring and tedious and makes people hate math.
A Lean textbook!
Why no HoTT, though?
"Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?" https://news.ycombinator.com/item?id=43196452
Additional Lean resources from HN this week:
"100 theorems in Lean" https://news.ycombinator.com/item?id=44075061
"Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean" https://news.ycombinator.com/item?id=44119725
Very cool. Analysis I was the first "real" math textbook that I (an engineer, not a mathematician) felt like I could completely follow and work through, after a few attempts to get through others like Rudin. Hopefully the Lean companion will help make it even more accessible to people who are familiar with math and programming and looking to learn things rigorously.
Over the years there has been a steady stream of people attempting to formalize Tao's Analysis I book in Lean, i.e. doing exactly what Tao is doing now (unfortunately none of them go beyond the first few chapters -- I hope Tao can go further!). I was considering doing this myself, so that my Analysis I solutions blog [1] would be accompanied by formalized proofs of each exercise (which I thought people working through the book might find useful).
I already posted the following in the private Discord server for the book, but this seems like possibly a good public space to share the following, in case anyone here may find it useful:
- https://github.com/cruhland/lean4-analysis which pulls from https://github.com/cruhland/lean4-axiomatic
- https://github.com/Shaunticlair/tao-analysis-lean-practice
- https://github.com/vltanh/lean4-analysis-tao
- https://github.com/gabriel128/analysis_in_lean
- https://github.com/mk12/analysis-i
- https://github.com/melembroucarlitos/Tao_Analysis-LEAN
- https://github.com/leanprover-community/NNG4/ (this one does not follow Tao's book, but it's the Lean4 version of the natural numbers game, so has very similar content as Chapter 2)
- https://github.com/djvelleman/STG4/ (similar to the previous one, this is the Lean4 set theory game, so it's possibly similar content as Chapter 3; however, in https://github.com/djvelleman/STG4/blob/main/Game/Metadata.l... I see "import Mathlib.Data.Set.Basic" so this seems to just import the sets from Lean rather than defining it anew and setting down axioms, so this approach might mean that Lean will "know" too much about set theory, which is not good for our purposes)
- https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c... -- for constructing the integers
- https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- possibly the same file as above
- https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- for constructing the rationals
- https://lean-lang.org/theorem_proving_in_lean4/axioms_and_co... -- shows one way of defining a custom Set type
I am wondering how much this "prove isomorphism to Mathlib equivalent" is relevant. By this I mean, would anything change if the isomorphism part would be left out, i.e. is it actually used anywhere, for example for automatically translating theorems?
He didn't really fully explain why he chose Lean over Coq or Agda though.
Does anyone know a good starting point to try Lean for Linear Algebra?
[dead]
To me, the most exciting aspect of teaching mathematics using Lean is the immediate feedback. If a student's proof is wrong, it simply won't compile.
Previously, the only feedback students could receive would be from another human such as a TA, instructor, or other knowledgeable expert. Now they can receive rapid feedback from the Lean compiler.
In the future I hope there is an option for more instructive feedback from Lean's compiler in the spirit of how the Rust compiler offers suggestions to correct code. (This would probably require the use of dedicated LLMs though.)