4 ms·
Propositional logic exercises with the lean theorem prover
- sidpatil 5y agoJust the kind of thing I've been looking for!
- deleted 5y ago[deleted]
- mathematically 5y agoJust a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true.
- BreakfastB0b 5y agoIt’s probably supposed to be (P & R) <-> (Q & S)
- mathematically 5y agoYup, transposition error.
- kevinbuzzard 5y agoThanks so much! Fixed.
- kevinbuzzard 5y agoPS 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.
- mathematically 5y agoIt's very fun. Thanks for putting it together.
- giomasce 5y agoSee also the Natural Number Game.