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).
"Migration controls serve as a blindfold, enabling Americans to ignore most of the poverty, deprivation, and vulnerability that exist in the world by keeping it physically at a distance. In the past, people lived without this blindfold. The wealthy lived amidst poverty, sometimes engaging in generous charity to the poor, sometimes learning, perhaps callously, to ignore them.
Citizens of a modern welfare state, by contrast, feel that the state should coerce people to give to the poor so as to remove from the streets the kind of visible poverty that would make them feel obliged to give, allowing them to feel conscientious and affluent at once. The price of this moral complacency is paid by would-be immigrants who are not allowed to come to America to better their condition by honest labor, lest their poverty trouble the consciences of affluent Americans."
"Gradual expansion and merging of free migration zones: For instance, the EU is a free migration zone for European countries, and it is gradually adding countries. Suppose the United States and Canada created their own free migration zone, Southeast Asian countries created their own free migration zone, and a few free migration zones emerged in Africa and Latin America (South America). The US-Canada free migration zone could, after some time, add Mexico and the Caribbean Islands, and then merge with the South American free migration zone. The European free migration zone could eventually merge with the new unified American migration zone. Over time, as the threat of terrorism, and the subjective sense of the threat, receded more and more into the past, the Gulf states could merge with the European free migration zone. And so on, until eventually the whole world would be a free migration zone."
"Now, the analogy between trade and migration is far from perfect. But I think that on the issue of reciprocity, the economists’ objection to mercantilist-style thinking in the trade context can be transferred to the migration context. In other words, unilateral open immigration generates net benefits, even if other countries don’t follow suit. Thinking of immigration law in reciprocity terms is fundamentally misguided."
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/