Is this correct? Here's my reasoning.

(Definition) Math is anything that can be proved from axioms.

(Assumption) All (finite length) axiom sets can be enumerated.

(Assumption) All (finite length machine decide-able) proofs can be enumerated. (Enumerate through axiom sets, shortest first; enumerate through proofs shortest first).

By enumerating through all proofs (and axioms) and verifying each proof for correctness you can output all valid (axiom set, proof) tuples.

Does this automate math?

Another way of looking at it is enumerating through all possible Metamath programs shortest to longest program length and evaluating for correctness. http://us.metamath.org/

  • $\begingroup$ Well, yea. But it may not be the best way to actually automate maths, as you won't use theorems \ lemmas when you prove something. $\endgroup$
    – nir shahar
    Sep 4, 2021 at 17:22
  • $\begingroup$ @JohnL. the OP did define "math" as what can be produced by this system. I understood "automating maths" as - "finding all possible proofs for all possible provable statements". Therefore I think it means that "maths" can be enumerated, or equivalently - the problem of asking if a specific statement is correct is in $RE$ (can be solved using a TM that may not halt) $\endgroup$
    – nir shahar
    Sep 4, 2021 at 18:48
  • $\begingroup$ The system will also produce trivial useless results and that also in extremely large amount, possibly unbounded. For example: $1+1 = 2$ or $1+1+\dotsc+n$ times $= n$. $\endgroup$ Sep 4, 2021 at 19:21
  • $\begingroup$ @InuyashaYagami Agreed. I thought this was a starting point: start with brute force, then make it more elegant. If we can enumerate through all provable statements and their proofs, then it becomes a problem of finding "interesting" theorems and their proofs. $\endgroup$ Sep 4, 2021 at 20:00
  • 1
    $\begingroup$ You might want to take a look at formal logic. There is a bunch of stuff like this in that area. And, its a completely formal system! I'm certain there are automated proof systems with more intelligent behavior than just searching every possible proof, but I don't have the knowledge required for such complicated systems, so I can't help you with that. Good luck :) $\endgroup$
    – nir shahar
    Sep 4, 2021 at 21:00


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.