💾 Archived View for gemlog.blue › users › jiaming › 1605385423.gmi captured on 2021-12-04 at 18:04:22. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
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