# Why isn't math proofs just a computer trial and error?

I already asked a similar question, but I recently began a course of Logic and it gave me not an answeat but a refination of my question, which I redefine here.

My thinking is the following:

Suppose we have a limited set of $$n$$ symbols {$$\forall$$, $$\neg$$, ...} and some statements {$$P$$, $$Q$$, ..., $$Z$$} made with the symbols and assumed True, therefore Axioms.

Now suppose that we want to prove a statement $$A$$, that means, we want to start at the Axioms and arrive at $$A$$ using only a logic combination of our symbols.

My question is: why not set a computer to try every possible path?

To clarify, we want something like $$P \land Q \land \text{...} \land Z \to \text{(?)} \to A$$, so my question is: why not set a computer to change the $$(?)$$ to one of each of the $$n$$ symbols from {$$\forall$$, $$\neg$$, ...}, then if it doesn't work go for two symbols, then for three.

It is curious because as I am writing this, I realized that the Time Complexity of this proccess would be indeed complex. However, I stand my question, because for example if the problem is an important one like the Goldbach Conjecture, why not set a lot of computers to optimize the proccess, and if we will inevitably do it someday why not do it already, as we need to start sometime? Speaking of that, one thing I would also like to know is if Quantum Computing would help this cause I proposed, making Math just a matter of combinatorical computer trial and error.

My questioning is somewhat vague, but any glimpsy of why Math proofs can't work like that would be of great value.

• The problem here is en.wikipedia.org/wiki/Halting_problem . You could set up such a system, but all it would tell you is after a certain run time, it hasn't found a proof or counter-proof that is under $n$ instructions long. There'd be tons of cases where the program wouldn't complete
– Alan
Aug 3, 2021 at 13:12
• To me, this is kind of like asking "why can't a computer design a space shuttle?" There's just an incredible amount of ingenuity and collaboration needed to do mathematics, and those are human qualities. Aug 3, 2021 at 13:17
• I pray to whatever deity is out there that we never automate the process of making mathematical proofs. What a dull world that would be for the advancement of human understanding. Aug 3, 2021 at 13:24
• @SeraPhim The power of computers will unfortunately still increase, we won't be able to prevent it. This has not only positive consequences, but too many humans force this evolution. We have to live with the drawbacks. The "deity" did not spare us from Corona either, I have little hope that this is better in any other area of life. Aug 3, 2021 at 13:42
• To the OP: there is a large literature on automated reasoning. I think the Goldbach conjecture is likely to be way out of reach for current techniques (including techniques involving quantum computing),but it's a good thing to think about for the future. Aug 6, 2021 at 22:20

Computers are fast. Rugged fast. And yet, breaking into my social media accounts by guessing my password, 10+ characters long with letters and digits, requires at most $$62^{10} \approx 10^{17}$$ guesses, which at a rate of 1000 attempts per second would take 300 000 years. Getting a second computer wouldn't make a dent into that for any person alive. Getting a thousand computers wouldn't really matter either, we're still talking centuries.