Propositional logic exercises with the lean theorem prover (github.com) 54 points by mathematically 4y ago ↗ HN
[–] sidpatil 4y ago ↗ Just the kind of thing I've been looking for! [–] [deleted] 4y ago ↗ (comment deleted) [–] mathematically 4y ago ↗ Just a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true. [–] BreakfastB0b 4y ago ↗ It’s probably supposed to be (P & R) <-> (Q & S) [–] mathematically 4y ago ↗ Yup, transposition error. [–] kevinbuzzard 4y ago ↗ Thanks so much! Fixed. [–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
[–] mathematically 4y ago ↗ Just a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true. [–] BreakfastB0b 4y ago ↗ It’s probably supposed to be (P & R) <-> (Q & S) [–] mathematically 4y ago ↗ Yup, transposition error. [–] kevinbuzzard 4y ago ↗ Thanks so much! Fixed. [–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
[–] BreakfastB0b 4y ago ↗ It’s probably supposed to be (P & R) <-> (Q & S) [–] mathematically 4y ago ↗ Yup, transposition error. [–] kevinbuzzard 4y ago ↗ Thanks so much! Fixed. [–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
[–] mathematically 4y ago ↗ Yup, transposition error. [–] kevinbuzzard 4y ago ↗ Thanks so much! Fixed. [–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
[–] kevinbuzzard 4y ago ↗ Thanks so much! Fixed. [–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
[–] kevinbuzzard 4y ago ↗ 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. [–] mathematically 4y ago ↗ It's very fun. Thanks for putting it together.
9 comments
[ 3.6 ms ] story [ 26.4 ms ] thread