Skip to content

Propositional logic exercises with the lean theorem prover

github.com/ImperialCollegeLondon
54 pointsmathematically8 comments
On HN

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.

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.