Natural Number Game: build the basic theory of the natural numbers from scratch

Re:Natural Number Game: build the basic theory of the natura... by Animats on Tuesday December 17, 2024 @12:58PM (#42443539)

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

[ Parent | on HN ]

Re:Natural Number Game: build the basic theory of the natura... by anthk on Tuesday December 17, 2024 @02:56PM (#42444672)

Under SBCL it would run even faster.

Also, not CL, but I've got bored with Scheme and computer abstractions requiring you to proof every step on recursion by induction. I just put a base case at f(0) with an invariant and I tested it against f(1).

[ Parent | on HN ]

Re:Natural Number Game: build the basic theory of the natura... by specialgoodness on Wednesday December 18, 2024 @11:35AM (#42451999)

Beautiful! Imandra is a modern Boyer-Moore style theorem prover for higher-order functional programming (its logic is based on a typed higher-order subset of OCaml rather than Boyer-Moore's basis on an untyped first-order subset of Pure Lisp (and later Common Lisp with ACL2)), but there are a lot of similarities! It also integrates computable counterexamples in a really cool way (they're first-class values reflected in the runtime and you can directly compute with them, including counterexamples to higher-order goals which involves function synthesis!). Imandra is used a lot for formal verification in finance, for example.

[ Parent | on HN ]