Hacker News new | past | comments | ask | show | jobs | submit login
Propositional logic exercises with the lean theorem prover (github.com/imperialcollegelondon)
54 points by mathematically 3 months ago | 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.




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

Search: