Hacker News Reader

Comment by antman | Hacker News Reader

I can't wrap myself around how theorem provers work. Is there something like a beginner tutorial with examples from simple uses? And which theorem prover would be intuitive for an introduction to this space?

View on HN

Yes, this exists. it is called the "Natural Number Game" and interactively teaches you to use the Lean theorem prover to prove simple theorems about addition, multiplication, and so on. It runs in the browser.

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...

I highly recommend Software Foundations Volume 1: Logical Foundations as an introduction to theorem proving in Coq. Try working through the first few chapters and see what you think: https://softwarefoundations.cis.upenn.edu/lf-current/toc.htm...

This probably isn't a simple nor use-friendly intro, but it's pretty comprehensive at least: https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf (section 1.2 has the first minimal proof, although familiarity with formal logic is kind of a pre-req to properly parsing this style of writing)

I remember learning and using Coq in a similar 300-level CS course at my university, 10+ years ago.

Start with the idea x=a+c. x can now be short hand for a+c. That may help? If you think of a theorem in the light that it is a giant function you can break it down that way too. Like sprintf is shorthand for the monster of bit of code that is sprintf.

The Little Prover might be a good choice: it’s about ACL2, which was used to prove various floating point implementations were correct. It’s a fairly accessible guide to proving theorems in this system.

Reply on news.ycombinator.com