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.
Similar to the system gwern mentioned in a sibling comment, I have implemented a "spaced inbox" system [1] that shows me old notes that I have written. The idea is to encourage me to keep adding to and refining ideas I have (but of course, the scheduling can be tweaked to only show notes that I am likely to have forgotten, as gwern suggests). Perhaps coincidentally, both my spaced inbox system and the Remembrance Agent in the OP are designed to work with Emacs (though mine does not force the user to use Emacs).
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/