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