Propositional logic exercises with the lean theorem prover

Built with the HackerNews API. Developed by LJT.AI

Note: The HackerNews API provides up to 500 stories per category

Propositional logic exercises with the lean theorem prover | Dark Hacker News

54 points by mathematically 4 years ago | 8 comments

giomasce 4 years ago |

See also the Natural Number Game.

sidpatil 4 years ago |

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

mathematically 4 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 4 years ago | | |

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

mathematically 4 years ago | | |

Yup, transposition error.

kevinbuzzard 4 years ago | | |

Thanks so much! Fixed.

kevinbuzzard 4 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.

mathematically 4 years ago | | |

Yup, transposition error.

kevinbuzzard 4 years ago | | |

Thanks so much! Fixed.

kevinbuzzard 4 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.

mathematically 4 years ago | | |

It's very fun. Thanks for putting it together.

mathematically 4 years ago | | |

It's very fun. Thanks for putting it together.