Skip to content

Top New Best Ask Show Jobs

Propositional logic exercises with the lean theorem prover | Better HN

Propositional logic exercises with the lean theorem prover (opens in new tab)

(github.com)

54 pointsmathematically4y ago8 comments

8 comments

See also the Natural Number Game.

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

mathematicallyOP4y ago

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

BreakfastB0b4y ago

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

j / k navigate · click thread line to collapse