Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
Propositional logic exercises with the lean theorem prover (github.com/imperialcollegelondon)
54 points by mathematically on Oct 21, 2021 | hide | past | favorite | 8 comments


See also the Natural Number Game.


Just the kind of thing I've been looking for!


Just a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true.


It’s probably supposed to be (P & R) <-> (Q & S)


Yup, transposition error.


Thanks so much! Fixed.


PS I cannot believe my undergraduate teaching material is on HN! I am a math lecturer and this is just my course notes for my UGs.


It's very fun. Thanks for putting it together.




Consider applying for YC's Winter 2026 batch! Applications are open till Nov 10

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: