This is very like Boyer-Moore theory[1], which builds up mathematics from the Peano axiom level. Boyer and Moore wrote an automated theorem prover that goes wi

This is very like Boyer-Moore theory[1], which builds up mathematics from the Peano axiom level. Boyer and Moore wrote an automated theorem prover that goes with this theory. I have a working copy for GNU Common LISP at [2]. "It is perhaps easiest to think of our program much as one would think of a reasonably good mathematics student: given the axioms of Peano, he could hardly be expected to prove (much less discover) the prime factorization theorem. However, he could cope quite well if given the axioms of Peano and a list of theorems to prove (e.g., “prove that addition is commutative,” . . . “prove that multiplication distributes over addition,” . . . “prove that the result returned by the GCD function divides both of its arguments,” . . . “prove that if the products over two sequences of primes are identical, then the two sequences are permutations of one another”)." - Boyer and Moore [1] https://www.cs.utexas.edu/~boyer/acl.pdf https://www.cs.utexas.edu/~boyer/acl.pdf [2] https://github.com/John-Nagle/nqthm/tree/master https://github.com/John-Nagle/nqthm/tree/master