💾 Archived View for gemlog.blue › users › jiaming › 1605385423.gmi captured on 2022-07-16 at 17:34:18. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2021-12-04)
-=-=-=-=-=-=-
14/11/2020 (Things I learned)
- the details of basic propositional logic, gamified iset.mm with a piton script
- Metamath ACTUALLY relies on meta unformalised "soundness" proofs to know that
definitions are eliminable and conservative.
- iset.mm is MUCH smaller than set.mm
- Metamath proofs are super hard to shorten
- youtube tries to stalk you through your IP if you try to avoid them?? WTF
- pigeons still get fed after being able to walk and play and spread their wings
- silence (no building construction music) feels great
- sambal ikan keli can scare the lausai demon away