It has not been proven that a computer cannot do math better than a person. Let's say in the future a computer is the first to prove the Riemann Hypothesis. Most people would say that the computer is then better at math than a human.
We don't know exactly how good people are at this. Perhaps there's some tier of intelligence that is better than people but worse than the all-powerful algorithm that Gödel proved can't exist.
For instance, a machine that is merely faster would be better than we are. A machine that could instantly simulate an entire civilization from the beginning of time, generate entire generations of mathematicians, and simulate their thinking for thousands of subjective years and then hand you back the results of their thinking would be better at it than we are, even if it wouldn't be better in the sense of being able to deterministically decide whether there's an answer or not.
Have you got some links? Sounds very interesting.
https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Arguably, humans require more energy per operation. So, presumably such an argument hinges upon what types of operations are performed in conducting automated proof search?
The context here is that certain problems cannot be solved by an algorithm, which doesn't necessarily translate into "cannot be performed by a machine".
It only means that there cannot be any Turing machine capable of solving them, no matter what "operations" it represents.
But there are real-world instances that contradict this hypothesis already. Humans don't exhibit Turing-computable behaviour because they did indeed solve problems that aren't solvable by Turing Machines.
I can give a very concrete example as well. Consider the following program (in Python for simplicity's sake):
def nat(x):
yield x
yield from nat(x+1)
for a in nat(2):
for b in nat(2):
for c in nat(2):
if a*a*a + b*b*b == c*c*c:
print(f"{a}^3 * {b}^3 = {c}^3")
exit()
Yet it has has been proven centuries ago that the above program won't halt.
The mathematicians couldn't have used a Turing Machine-compliant computation, so something else must be involved.
Now this of course doesn't mean that humans are generally capable of solving every problem that's not solvable by an algorithm, but it means that they can solve problems that algorithms can't solve.
Yes, there is. There's a machine which does nothing but print that exact proof.
You seem to have conflated solving an instance of a problem with solving the entire problem. Turing's theorem states that no one Turing machine will get the answer right for every instance of the halting problem, but for any instance that one specific machine gets wrong, there's another machine that also gets that instance right (in addition to everything else the original machine gets right).
Either the (unreferenced) study was actually arguing that "automated proof search" can't be done at all, or that human neural computation is categorically non-algorothmic.
Grid search of all combinations of bits that correspond to [symbolic] classical or quantum models.
Or better: evolutionary algorithms and/or neural nets.
I don't quite understand the role of neural nets in that context, though. Those just classical computations in the end and should be bound by the same limits that every other algorithms are, shouldn't they?
Neuromorphic engineering has expanded since the 1980s. https://en.wikipedia.org/wiki/Neuromorphic_engineering
Quantum computing is the best known method for simulating chemical reactions and thereby possibly also neurochemical reactions. But, Is quantum computing necessary to functionally emulate human cognition?
It may be that a different computation medium can accomplish the same tasks without emulating all of the complexity of the brain.
If the brain is only classical and some people are using their brains to perform quantum computations, there may be something there.
Quantum cognition: https://en.wikipedia.org/wiki/Quantum_cognition
From "Quantum Memristors in Frequency-Entangled Optical Fields" (2020) https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7079656/ :
> Apart from the advantages of using these devices for computation [12] (such as energy efficiency [13], compared to transistor-based computers), memristors can be also used in machine learning schemes [14,15]. The relevance of the memristor lies in its ubiquitous presence in models which describe natural processes, especially those involving biological systems. For example, memristors inherently describe voltage-dependent ion-channel conductances in the axon membrane in neurons, present in the Hodgkin–Huxley model [16,17].
> Due to the inherent linearity of quantum mechanics, it is not straightforward to describe a dissipative non-linear memory element, such as the memristor, in the quantum realm, since nonlinearities usually lead to the violation of fundamental quantum principles, such as no-cloning theorem. Nonetheless, the challenge was already constructively addressed in Ref. [18]. This consists of a harmonic oscillator coupled to a dissipative environment, where the coupling is changed based on the results of a weak measurement scheme with classical feedback. As a result of the development of quantum platforms in recent years, and their improvement in controllability and scalability, different constructions of a quantum memristor in such platforms have been presented. There is a proposal for implementing it in superconducting circuits [7], exploiting memory effects that naturally arise in Josephson junctions. The second proposal is based on integrated photonics [19]: a Mach–Zehnder interferometer can behave as a beam splitter with a tunable reflectivity by introducing a phase in one of the beams, which can be manipulated to study the system as a quantum memristor subject to different quantum state inputs.
Quantum harmonic oscillators have also found application in modeling financial markets. Quantum harmonic oscillator: https://en.wikipedia.org/wiki/Quantum_harmonic_oscillator
One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate.
Another results showed that the complexity of general automated proof generation is exponential in nature.
Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.)
A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1].
This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving.
A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP.
[1] https://en.wikipedia.org/wiki/List_of_undecidable_problems
Which humans can not do.
And yes, humans are very well capable of solving that, because humans can in fact proof whether any program halts.
This doesn't mean every human can or that it has been done for every program, but it means that humans are - in general - able capable of deciding this, while algorithms (programs) can't.
For now at least, we don't know of any counter-example to the Church-Turing thesis. Humans are certainly not able to tell whether a program in general will halt for any input it recieves. If you believe otherwise, please tell me whether the following program halts:
Foo():
if P = NP:
return true
else:
Foo()That's a logical fallacy - just because I can't show whether P=NP doesn't mean nobody can!
Turing-Church is a conjecture, not a theorem. There have been arguments made against it [1].
Also, the link you replied provides an argument of efficiency, not an argument of possibility. It is arguing that we might use things that are not Turing machines because they can solve the problem more efficiently, not because they can solve problems Turing machines could never hope to solve.
If there is a single Turing machine for which there is no human that can tell whether it will halt, the conjecture that human reasoning is not more powerful than Turing machines is still not disproven.
Also, if you were right that humans can do things that Turing machines can't, it would be an interesting excersise to try to find that example of super-Turing human reasoning and try to see why it can't be encoded as a Turing machine. No one has successfully done this yet, so there is no reason to believe that it is possible.
The "given any program" part is crucial.
And we aren’t doing some kind of magical logic when we humans create proofs. Sure naively general automated proof generation could be exponential in nature, but that hasn’t stopped us from mathematics research. There’s no reason it should stop computers either.
Humans can solve problems that aren't solvable by algorithms and that's why humans can - in general - decide whether a given program will halt. That doesn't mean every human can or that it has been done for every program (which would be impossible, since there are infinitely many instances anyway).
But the difference between humans and Turing Machines (computers) is, that humans can and did proof undecidable problems, while algorithms provably can't.
This is a fundamental difference and there's no way around it. So whatever might be done in ATP, it can't be algorithmic in nature or based on a Turing Machine in order to be applied universally.
Unless of course, you know of a way to disprove Gödel and Turing...
Basically, why can't I write an algorithm that can be given input for "is the halting problem decidable?" and return "no"?
One possible reason why mathematics cannot be automated is because some important piece of contemporary mathematics is fundamentally unsound, e.g. ∞, LEM, AOC. Mathematicians are very clever at building and manipulating formal systems, but are prone to mistakes and must accept on faith some foundations to make any progress. If you spent your entire career building a castle and someone like Gödel or Brouwer came along and claimed the whole thing is built on sand, naturally you (and all your venerable castle-building colleagues) would be unwilling to simply accept this development and move on.
I suspect what many people call mathematics today lost its course somewhere after Cantor, who was a supremely clever human being, but either mentally unstable or driven to madness trying to operationalize infinite sets. If our universe were infinite, maybe his ideas would be valid, but even then we could never build machines to verify those claims. While it has produced an abundance of useful ideas, it also generates a number of paradoxes (e.g. Zeno, Banach-Tarski), which are simply incompatible with the universe in which we live.
What we can automate, and have successfully automated many times over, is proof checking. In that sense, yes, computers have already fully automated mathematical reasoning, because checking proofs is fully formalized and mechanized.
I think that what people really ought to be asking for is the ease with which we find new results and communicate them to others. In that sense, computer-aided proofs can be hard to read and so there is much work to be done in making them easier to communicate to humans. Similarly, there is interesting work being done on how to make computer-generated proofs which use extremely-high-level axiom schemata to generate human-like handwaving abstractions.
I'm still not sure how I feel about the ATP/ITP terminology used here. ATPs are either of the weak sort that crunch through SAT, graphs, and other complete-but-hard problems, or the strong sort which are impossible. Meanwhile, folks have drifted from "interactive" to "assistant", and talk of "proof assistants" as tools which, like a human, can write down and look at sections of a proof in isolation, but cannot summon complete arbitrary proofs from its own mind.
Edit: One edit will be quicker than two replies and I tend to be "posting too fast". The main point is captured well by [0], but they immediately link to [1], the central result, which links to [2], an important corollary. At this point, I'm just going to quote WP:
> The first [Gödel] incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e., an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
> The second [Gödel] incompleteness theorem, an extension of the first, shows that the system cannot demonstrate its own consistency.
> Informally, [Tarski's Undefinability] theorem states that arithmetical truth cannot be defined in arithmetic.
I recognize that these statements may seem surprising, but they are provable and you should convince yourself of them. I recently reviewed [3] and found it to be a very precise and complete introduction to all of the relevant ideas; there's also GEB if you want something more fun.
[0] https://en.wikipedia.org/wiki/Automated_theorem_proving#Deci...
[1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
[2] https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...
[3] https://www.logicmatters.net/resources/pdfs/godelbook/GodelB...