Propositional logic exercises with the lean theorem prover

54 points by mathematically 5 years ago · 9 comments

Reader

2 threads

giomasce 5 years ago

See also the Natural Number Game.

sidpatil 5 years ago

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

mathematicallyOP 5 years 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 5 years ago
  
  It’s probably supposed to be (P & R) <-> (Q & S)
  - mathematicallyOP 5 years ago
    
    Yup, transposition error.
    
    kevinbuzzard 5 years ago
    
    Thanks so much! Fixed.
    
    kevinbuzzard 5 years 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.
    
    mathematicallyOP 5 years ago
    
    It's very fun. Thanks for putting it together.