Is someone trying to solve problems by building all possible proofs using all possible rules of inference?

Question

We obviously can construct a program that, starting with ZFC (or any other theory) axioms, would use all possible rules of inference to get all possible proofs constructible in ZFC. (There would be countably many such proofs.)

Now, with a Turing Machine capable of solving the Halting Problem, we would be able to easily decide upon every problem this way.

Of course we do not have one, but my question is:

Did someone actually build a program that is going through all those rules of inference, with the purpose of finding proofs of, say, the 20 most important problems in math? Without our 'halting machine' this proces can possibly take forever, but maybe we will stumble upon some of those proofs.

Answer 1

Well, there is a Turing machine which halts iff ZFC is inconsistent. There are cited papers and blogposts, but it is related to the paper:

• Adam Yedidia and Scott Aaranson, A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory

There is a well-commented program, based on similar principles, with comments explaining the encoding of logic and ZF axioms:

• https://github.com/sorear/metamath-turing-machines/blob/master/zf2.nql

Answer 2

This is called proof search, but the combinatorial explosion of possible proofs (and resulting "junk theorems") makes it practically impossible to find anything interesting by brute force.

Imagine your proof search program makes its choices by reading bits from a random number generator. Even if this is done efficiently, there are so many choices at each step that even a theorem we consider simple will use hundreds or thousands of bits. After a few hundred bits, there are already more possible proofs than atoms in the universe. Cracking an NSA-grade encryption key amounts to correctly guessing a 384-bit number.

So we need smarter ways to narrow the search instead of just using brute force. This is an active research area, and AI approaches are promising. See e.g. https://arxiv.org/abs/1701.06972 .