3
$\begingroup$

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.

$\endgroup$
11
  • 8
    $\begingroup$ 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 $\endgroup$
    – Alan
    Aug 3, 2021 at 13:12
  • 3
    $\begingroup$ 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. $\endgroup$
    – Randall
    Aug 3, 2021 at 13:17
  • 3
    $\begingroup$ 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. $\endgroup$
    – SeraPhim
    Aug 3, 2021 at 13:24
  • 1
    $\begingroup$ @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. $\endgroup$
    – Peter
    Aug 3, 2021 at 13:42
  • 1
    $\begingroup$ 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. $\endgroup$
    – Rob Arthan
    Aug 6, 2021 at 22:20

1 Answer 1

Reset to default
5
$\begingroup$

This absolutely works in theory. The problem is the number of computers needed ("a lot") is in practice "too many".

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.

A mathematical proof, written in first or second order logic is a lot longer than my social media password, and requires more time to verify whether a step was correct or not. A thousand or a million computers or more would cost a fortune, and would still not be likely to produce results the programmer of the computer will be alive to see. The investment into flesh-and-blood mathematicians would yield a much higher return on investment.

That said, computers absolutely are useful for assisting with well-defined parts of mathematical proofs, going back to the controversy regarding the proof of the Four color theorem in 1976.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .