| 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 [1] https://taoanalysis.wordpress.com/ |