| Here's the Boyer-Moore theorem prover[1] from around 1980 doing that.[2] The proofs are fully automatic but you have to ask it to prove the theorems in an order so that the theorems you need for each step are already done. Otherwise it gets lost trying different paths. This is runnable; 8 years ago I ported it to GNU Common LISP. Takes under a second now. Took 45 minutes in 1980. This is pure constructive mathematics. No existence proofs. Everything is computable. The first theorem: X + 0 = X In Boyer-Moore notation: (PROVE-LEMMA PLUS-0 (REWRITE)
(EQUAL
(PLUS X 0)
(FIX X)))
FIX is just if it's a number, then the number, else 0. That makes the function total.The second theorem: X + (Y + 1) = (1 + (X + Y) (PROVE-LEMMA PLUS-ADD1 (REWRITE)
(EQUAL
(PLUS X (ADD1 Y))
(IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X))))
ADD1 is a primitive of Boyer-Moore theory. ADD is actually recursive ADD1.The user just lists the proof goals. Here's the input file.[3] The proofs are all automatic.
This is more automation than many modern provers seem to have. Toward the end, it proves McCarthy's theory of arrays, something I wrote. McCarthy stated those as axioms, but they are in fact provable. The proofs are clunky because there's no set theory yet. I should have built up constructive set theory first, but I didn't realize that back then. [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... [3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp... |