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 (unfortu

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/