Hacker News Reader

It is true that Godel's incompleteness theorem states that there is no complete axiomatization of arithmetic; no first order axioms can characterize the natural numbers up to isomorphism. But Godel's completeness theorem ( https://en.wikipedia.org/wiki/Gödel%27s_completeness_theorem) states that first order logic is in fact complete as a deductive system, and most automated theorem provers have the property that if a proof exists, given enough time they will eventually find it. In higher order logic the situation is reverse: the proof theory is incomplete, but you can eg characterize the natural numbers up to isomorphism. Anyway, I believe that many of your critiques apply to formal logic itself, not so much the attempts to automate formal logic.

The ATP/ITP distinction is pretty old and standard. It is more blurred these days when ITPs like Isabelle include ATPs to help making the size of a reasoning step more human-like.

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 cannot just ask a computer to find a proof or refutation of Goldbach's Conjecture or other "Goldbach-type" statement and have it do any better than a person

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.

A fully generalized automated "proof checking" is also impossible because it depends on what system of axioms and rules the checking algorithm is using, which is, again, limited by incompleteness theorems. BTW if we have a proof checking algorithm in some axiomatic system then it's pretty easy to write a proof finding algorithm in this system. Via a brute-force - it just checks all strings as a possible proofs of a statement and simultaneously all strings as a proof of negation. It will definitely stop if there is a proof of the statement or its negation, but will run infinitely if both proofs are missing.

> a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible

Have you got some links? Sounds very interesting.

He is refering to the late 19th and early 20th century work on the foundations of mathematics amoung mathematicans and philosophers. They attempted to fully formalise mathematics. Serveral approaches and schools in mathematics all hit various paradoxes, often of the same kind, and this ultimately culminated in Godel's incompleteness theorems:

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

https://plato.stanford.edu/entries/goedel-incompleteness

There's also a thing called "the halting problem" which is related to this. Because without the halting problem you could solve any mathematical proof by simply turning it into a computer program that brute forces the problem domain and calculating whether the the program will terminate or not. Of course, this is impossible.

That's a bit backwards. The halting problem is a computer-flavored variant of Gödel's work. A very simple part -- it's essentially a computer program that says "The program that produced this string is lying".

As someone unfamiliar with the results you describe, why can’t a machine do better than a human? A smart human is better at writing proofs than a dumb one. If we had a highly advanced general artificial intelligence, why couldn’t it generate better results than the smart humans?

I don't know what result they were referring to, but I've often heard it said that AI of current types so never be capable of the same types of cognition that we can do. That's not to say we can't create a different type of AI, but at the moment that's just science fiction and will need some major advances in technology.

Or is automated proof search impossible for humans as well?

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?

What would "automated proof search" even mean in the context of being performed by a human being?

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.

The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans. That is, there are programs whose halting behavior no human will ever determine, theorems of Peano arithmetic whose proof no human will ever find, etc., no matter how much humans work at it.

> The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans.

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()

There is no Turing Machine capable of proving that this program won't halt (technically it will, due to practical limitations).

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.

> There is no Turing Machine capable of proving that this program won't halt

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).

The task (in terms of constructor theory) is: Find the functions that sufficiently approximate the observations and record their reproducible derivations.

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.

Roger Penrose argues that human neural computation is indeed non-algorithmic in nature (see his book "The Emperor's New Mind"; 1989) and speculates that quantum processes are involved.

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?

That human cognition is quantum in nature - that e.g. entanglement is necessary - may be unfalsifiable.

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

Quantum memristors are still elusive.

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

It has been shown numerous times that there are limits to automated proof generation.

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

Humans are not able to solve the halting problem. The halting problem isn't a question of if you can decide that some programs will not halt, but that you can decide if all programs would halt.

Which humans can not do.

No - that's simply not true. The Halting Problem states that there is no Turing Machine (i.e. program) capable of deciding whether a given program will halt.

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.

The Church-Turing thesis claims (and is believed to be right) that a Turing machine can solve (compute) any problem that can be solved (is computable).

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()

> If you believe otherwise, please tell me whether the following program halts

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].

[1] https://arxiv.org/ftp/cs/papers/0207/0207055.pdf

There is no reason to believe that the human mind can solve a superset of the problems solvable by a Turing machine, and a lot of evidence to the contrary.

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.

No, the correct statement is that there is no Turing Machine that can, given any program, decide whether it will halt.

The "given any program" part is crucial.

A human is no more capable of solving the halting problem than a computer.

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.

But we are (in general).

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...

I don't know what made you believe this, but humans are not magical. We absolutely can't solve the halting problem, and by definition nothing can decide an undecidable problem. As far as we know so far, the human mind is a (limited) Turing machine. In fact, as far as we know, there is no computing system more powerful than a Turing machine.

Are there any problems we have a proof for, and a corresponding proof that no algorithm can exist to provide said proof?

Basically, why can't I write an algorithm that can be given input for "is the halting problem decidable?" and return "no"?

Which undecidable theorems have humans proven?

yeah that's not a thing. Humans do regularly "solve" undecidable theorems, if by solve you mean "come up with heuristics that are good enough". Possibly even "provably good enough", as in "if there's a flaw in the algorithm, the lower bound on the badness of the input to make it unreachable in the lifetime of the universe".

> Computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated.

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.

Unsound with respect to what?

It's hard to say that human math is unsound when it's not even well defined. Human math sits on a substantial foundation of faith, and always will.