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/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)
I also made a theoretical calculation like this a couple of years ago [1]. I didn't answer the question "Can you memorize an infinite number of facts?" but rather the question "If you add a constant number of cards to Anki each day, what does your daily review load look like in the limit?"
That is basically the typical accounting equation without the Equity term [1], so I am confused how you handle opening balances.
I think the problem with that scheme is that without some notion of debit/credit (or equivalently, transactions that sum to 0), you can't easily tell if your transactions are balancing. Somehow you have to encode the information that Assets are a "left hand side positive" account type, and that Income is a "right hand side positive" account type, which is what the "income is negative" stuff is doing. But now you have to remember which side of the equation the account is positive on.
I don't think it really helps to use negative numbers (e.g. thinking of income as negative is very confusing). I started a discussion [1] on the PTA subreddit about a month ago about how to make PTA syntax more intuitive, and someone suggested using arrows to mark the "from" (aka credit, or negative) and "to" (aka debit, or positive) accounts. The numbers are unsigned and the terms "credit" and "debit" aren't used, and I think it's way more intuitive.
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/