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