6 ms·

A Lean companion to Analysis I

292 points by jeremyscanvic 1y ago

danabramov 1y ago
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.
- dilawar 1y ago
  Same here. I learnt about convergence, Cauchy seq etc. it was published by a local non profit publisher -- Hindustan Book Agency so it was super affordable too.
  - smohare 1y ago
    [dead]
practal 1y ago
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?
- deleted 1y ago
  [deleted]
- titanomachy 1y ago
  If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest of the book.
  - danabramov 1y ago
    I loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalization could become if it strayed too far from Mathlib — but also was worried about losing the self-contained-ness if it just used Mathlib. This is a nice compromise imo.
- jhanschoo 1y ago
  I think that isomorphisms like this serve to establish 1. The development that you just did is equivalent to the corresponding object in Mathlib. Frequently, what is developed comes from concrete building blocks, whereas the corresponding definition in Mathlib might be a specialization of a complicated general class. 2. The basic notation and nomenclature for the object in Mathlib, which may differ.
nextos 1y ago
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 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.
- cole-k 1y ago
  I wouldn't be too surprised if PL proofs were simpler to start with. Part of what I hear people say is that they also are a lot more routine. Do structural induction, apply the IH to show an invariant holds, continue. I haven't done much theorem proving, nor have I done any "mathematical" (e.g. analysis) proofs with a theorem prover, but it makes me wonder how much skill transfer there is between them if "mathematical" proofs require a much different approach. I will also mention Software Foundations in Rocq (perhaps there is a Lean port). I worked through some of the first parts of it and found it quite pleasant.
  - crvdgc 1y ago
    Kevin Buzzard said something like the PL proofs are about deep structures on simple objects (mostly integers), while modern math mainly concerns complex objects. If you already have the definitions, the properties usually don't involve a lot of recursion and case analyses.
zozbot234 1y ago
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.
- smohare 1y ago
  As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers. I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.
  - thdhhghgbhy 1y ago
    Is there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.
- krapht 1y ago
  Certainly not for introductory courses. There's already too much on the table - how to prove, how to program, and the base material itself. I believe that's the experience of faculty who've tried as well - it's fine for advanced students, but a waste of instructional time for the average pupil.
ubj 1y ago
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.)
- vessenes 1y ago
  I’m yes on this, almost completely. But. I’m also thoughtful about proving things — my own math experience was decades ago, but I spent a lot of ‘slow thought’ time mulling over whatever my assignments were, trying things on paper, soaking up second hand smoke and coffee, your basic math paradise stuff. I wonder if using Lean here could lead to some flailing / random checking / spewing. I haven’t worked with Lean much, although I did do a few rounds with coq five or ten years ago; my memory is that I mostly futzed with it and tried things. Upshot - a solver might be great for a lot of things. But I wonder if it will cut out some of this slow thoughtful back-and-forth that leads to internalization, conceptualization, and sometimes new ideas. Any thoughts on this?
  - mseri 1y ago
    Jim Portegies (TU/e, Netherlands) and Jelle Wemmenhobe have done a lot of research on this, using their “waterproof” (controlled natural language compiled to coa) to test this directly in class. The results are very interesting, and indeed actively messing around is still a very important part of the learning experience, but you can see at least some benefits in also having a theorem prover to check if your proofs are correct. What I was surprised is that the students learn some patterns of proof properly, but only if you make sure that they are explicitly exposed by the proof assistant (so the more automation the less learning also in this case). You can find a lot of the work summarized in Jelle’s PhD thesis at https://research.tue.nl/nl/publications/waterproof-transforming-a-proof-assistant-into-an-educational-too https://research.tue.nl/nl/publications/waterproof-transform...
westurner 1y ago
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 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 https://news.ycombinator.com/item?id=44075061 "Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean" https://news.ycombinator.com/item?id=44119725 https://news.ycombinator.com/item?id=44119725
- krapht 1y ago
  Why should there be HoTT, though? A lot less work has gone into making HoTT theorem provers ergonomic to use. Also, the documentation is a lot more sparse. The benefits of HoTT are also unclear - it seems to only save work when dealing with very esoteric constructs in category theory.
- moomin 1y ago
  It’s an existing textbook, which answers the “Why not HoTT?” question. Although another might be that people doubt its pedagogical value.
- Mond_ 1y ago
  HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely close to being accepted as a reasonable standard, and it's kind of a non-starter for most people. This is a bit like asking the developers of a Javascript framework why they they didn't write a framework for Elm or Haskell.
  - zozbot234 1y ago
    > HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404
mettamage 1y ago
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. [1] https://www.youtube.com/@TerenceTao27 https://www.youtube.com/@TerenceTao27
brosco 1y ago
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.
jhanschoo 1y ago
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.
- ted_dunning 1y ago
  You can look for yourself. Much of the chapter on limits of real sequences is available in the sample pages. See here: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6 https://link.springer.com/chapter/10.1007/978-981-19-7261-4_...
IssaRice 1y ago
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 https://github.com/cruhland/lean4-analysis which pulls from https://github.com/cruhland/lean4-axiomatic https://github.com/cruhland/lean4-axiomatic - https://github.com/Shaunticlair/tao-analysis-lean-practice https://github.com/Shaunticlair/tao-analysis-lean-practice - https://github.com/vltanh/lean4-analysis-tao https://github.com/vltanh/lean4-analysis-tao - https://github.com/gabriel128/analysis_in_lean https://github.com/gabriel128/analysis_in_lean - https://github.com/mk12/analysis-i https://github.com/mk12/analysis-i - https://github.com/melembroucarlitos/Tao_Analysis-LEAN https://github.com/melembroucarlitos/Tao_Analysis-LEAN - https://github.com/leanprover-community/NNG4/ 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/ 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.lean 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/35bf66993e99cbcd8c9edc4914c9e7fc https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c... -- for constructing the integers - https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- possibly the same file as above - https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- for constructing the rationals - https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality https://lean-lang.org/theorem_proving_in_lean4/axioms_and_co... -- shows one way of defining a custom Set type [1] https://taoanalysis.wordpress.com/ https://taoanalysis.wordpress.com/
thdhhghgbhy 1y ago
He didn't really fully explain why he chose Lean over Coq or Agda though.
- _delirium 1y ago
  For this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1]. Now as to why he picked Lean a few years ago as his go-to theorem prover, I do think that would be an interesting backstory. As far as I know he hasn't written anything explicit about it. [1] E.g., https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
  - UltraSane 1y ago
    I would assume he chose Lean because it is what Kevin Buzzard has popularized and has been used to prove some very complex theories.
dfissadifdoi 1y ago
[dead]
331c8c71 1y ago
Does anyone know a good starting point to try Lean for Linear Algebra?
- griffzhowl 1y ago
  The canonical introduction is Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/index.html https://leanprover-community.github.io/mathematics_in_lean/i... It doesn't get to linear algebra till chapter 9, and it tends to be cumulative, but you could try the first 4 chapters to get the basics and jump ahead to see how you get on
UltraSane 1y ago
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.

292 points by jeremyscanvic 1y ago

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.

dilawar 1y ago
Same here. I learnt about convergence, Cauchy seq etc. it was published by a local non profit publisher -- Hindustan Book Agency so it was super affordable too.
- smohare 1y ago
  [dead]

practal 1y ago

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?

deleted 1y ago
[deleted]
titanomachy 1y ago
If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest of the book.
- danabramov 1y ago
  I loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalization could become if it strayed too far from Mathlib — but also was worried about losing the self-contained-ness if it just used Mathlib. This is a nice compromise imo.
jhanschoo 1y ago
I think that isomorphisms like this serve to establish 1. The development that you just did is equivalent to the corresponding object in Mathlib. Frequently, what is developed comes from concrete building blocks, whereas the corresponding definition in Mathlib might be a specialization of a complicated general class. 2. The basic notation and nomenclature for the object in Mathlib, which may differ.

nextos 1y ago

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 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.

cole-k 1y ago
I wouldn't be too surprised if PL proofs were simpler to start with. Part of what I hear people say is that they also are a lot more routine. Do structural induction, apply the IH to show an invariant holds, continue. I haven't done much theorem proving, nor have I done any "mathematical" (e.g. analysis) proofs with a theorem prover, but it makes me wonder how much skill transfer there is between them if "mathematical" proofs require a much different approach. I will also mention Software Foundations in Rocq (perhaps there is a Lean port). I worked through some of the first parts of it and found it quite pleasant.
- crvdgc 1y ago
  Kevin Buzzard said something like the PL proofs are about deep structures on simple objects (mostly integers), while modern math mainly concerns complex objects. If you already have the definitions, the properties usually don't involve a lot of recursion and case analyses.

zozbot234 1y ago

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.

smohare 1y ago
As a mathematician and also someone who has programmed for quite awhile I think any programmatic formalism will fail at inculcating the underlying understating. My bias of course is that I learned mathematical concepts via academic papers. I just feel that the overhead code presents is massive, since it often does not adhere to any semblance of style. I say say this as someone who has had to parse through other’s mathematical papers that were deemed incomprehensible. Code is 10x worse since there are virtually no standards with regards to comprehensibility.
- thdhhghgbhy 1y ago
  Is there not an idiomatic way to write proofs in Lean/Coq/Agda though? Idiomatic in the sense that once you learn the common idioms/tactics proofs become a degree more readable.
krapht 1y ago
Certainly not for introductory courses. There's already too much on the table - how to prove, how to program, and the base material itself. I believe that's the experience of faculty who've tried as well - it's fine for advanced students, but a waste of instructional time for the average pupil.

ubj 1y ago

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.)

vessenes 1y ago
I’m yes on this, almost completely. But. I’m also thoughtful about proving things — my own math experience was decades ago, but I spent a lot of ‘slow thought’ time mulling over whatever my assignments were, trying things on paper, soaking up second hand smoke and coffee, your basic math paradise stuff. I wonder if using Lean here could lead to some flailing / random checking / spewing. I haven’t worked with Lean much, although I did do a few rounds with coq five or ten years ago; my memory is that I mostly futzed with it and tried things. Upshot - a solver might be great for a lot of things. But I wonder if it will cut out some of this slow thoughtful back-and-forth that leads to internalization, conceptualization, and sometimes new ideas. Any thoughts on this?
- mseri 1y ago
  Jim Portegies (TU/e, Netherlands) and Jelle Wemmenhobe have done a lot of research on this, using their “waterproof” (controlled natural language compiled to coa) to test this directly in class. The results are very interesting, and indeed actively messing around is still a very important part of the learning experience, but you can see at least some benefits in also having a theorem prover to check if your proofs are correct. What I was surprised is that the students learn some patterns of proof properly, but only if you make sure that they are explicitly exposed by the proof assistant (so the more automation the less learning also in this case). You can find a lot of the work summarized in Jelle’s PhD thesis at https://research.tue.nl/nl/publications/waterproof-transforming-a-proof-assistant-into-an-educational-too https://research.tue.nl/nl/publications/waterproof-transform...

westurner 1y ago

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 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 https://news.ycombinator.com/item?id=44075061 "Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean" https://news.ycombinator.com/item?id=44119725 https://news.ycombinator.com/item?id=44119725

krapht 1y ago
Why should there be HoTT, though? A lot less work has gone into making HoTT theorem provers ergonomic to use. Also, the documentation is a lot more sparse. The benefits of HoTT are also unclear - it seems to only save work when dealing with very esoteric constructs in category theory.
moomin 1y ago
It’s an existing textbook, which answers the “Why not HoTT?” question. Although another might be that people doubt its pedagogical value.
Mond_ 1y ago
HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely close to being accepted as a reasonable standard, and it's kind of a non-starter for most people. This is a bit like asking the developers of a Javascript framework why they they didn't write a framework for Elm or Haskell.
- zozbot234 1y ago
  > HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404

mettamage 1y ago

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. [1] https://www.youtube.com/@TerenceTao27 https://www.youtube.com/@TerenceTao27

brosco 1y ago

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.

jhanschoo 1y ago

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.

ted_dunning 1y ago
You can look for yourself. Much of the chapter on limits of real sequences is available in the sample pages. See here: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6 https://link.springer.com/chapter/10.1007/978-981-19-7261-4_...

IssaRice 1y ago

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 https://github.com/cruhland/lean4-analysis which pulls from https://github.com/cruhland/lean4-axiomatic https://github.com/cruhland/lean4-axiomatic - https://github.com/Shaunticlair/tao-analysis-lean-practice https://github.com/Shaunticlair/tao-analysis-lean-practice - https://github.com/vltanh/lean4-analysis-tao https://github.com/vltanh/lean4-analysis-tao - https://github.com/gabriel128/analysis_in_lean https://github.com/gabriel128/analysis_in_lean - https://github.com/mk12/analysis-i https://github.com/mk12/analysis-i - https://github.com/melembroucarlitos/Tao_Analysis-LEAN https://github.com/melembroucarlitos/Tao_Analysis-LEAN - https://github.com/leanprover-community/NNG4/ 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/ 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.lean 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/35bf66993e99cbcd8c9edc4914c9e7fc https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c... -- for constructing the integers - https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- possibly the same file as above - https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- for constructing the rationals - https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality https://lean-lang.org/theorem_proving_in_lean4/axioms_and_co... -- shows one way of defining a custom Set type [1] https://taoanalysis.wordpress.com/ https://taoanalysis.wordpress.com/

thdhhghgbhy 1y ago

He didn't really fully explain why he chose Lean over Coq or Agda though.

_delirium 1y ago
For this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1]. Now as to why he picked Lean a few years ago as his go-to theorem prover, I do think that would be an interesting backstory. As far as I know he hasn't written anything explicit about it. [1] E.g., https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
- UltraSane 1y ago
  I would assume he chose Lean because it is what Kevin Buzzard has popularized and has been used to prove some very complex theories.

dfissadifdoi 1y ago

[dead]

331c8c71 1y ago

Does anyone know a good starting point to try Lean for Linear Algebra?

griffzhowl 1y ago
The canonical introduction is Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/index.html https://leanprover-community.github.io/mathematics_in_lean/i... It doesn't get to linear algebra till chapter 9, and it tends to be cumulative, but you could try the first 4 chapters to get the basics and jump ahead to see how you get on

UltraSane 1y ago

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.