How close are computers to automating mathematical reasoning? | Hacker News Reader

How close are computers to automating mathematical reasoning?

quantamagazine.org

100 pointsauggierose97 comments

People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as computer-based mathematicians. Both humans and computers are forced to work with a recursively enumerable set of axioms when constructing mathematical proofs, and so therefore are bound by the same limitations.

Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture.

In other words, using GIT when discussing proof automation is irrelevant.

I agree that GIT limits human provers as much as it limits automated ones, but I don't agree that it's irrelevant to the issue.

A human mathematician can lean on intuition in ways that a computer can't. Given a theorem that resists proof, a human might develop a feel for whether it's worth continuing to prove via conventional means or whether the troublesome territory is better approached from a different axiom set. That intuition may be driven by the problematic theorem being one of the true-but-unprovable ones that Godel assures us exists without that cause being apparent to the mathematician.

The automated prover, on the other hand, faces a halting problem here. Unless it is given some explicit reason to expect that the target is not attainable, it might try forever. So such a prover might need to be GIT-aware in ways that a human doesn't.

That's where ML comes in, to provide the 'intuition' for pruning the search space.

As a human this explanation is emotionally satisfying. It appeals to my sense of human exceptionalism. However how many true but unprovable theorems do we know about? Has anyone ever bothered to compile a list of true but unprovable under the axioms xyz? I would think it is exceedingly hard to manage such research as every axiom set xyz would require companion axioms abc to be provable, and such theorems (at least the non-trivial interesting ones) are possibly hard to reach.

This intuition for unprovableness may just be a mechanism for escaping local minima that gets lucky often enough.

Many such lists exist. For example: https://en.wikipedia.org/wiki/List_of_statements_independent...

That's certainly true, but Godel-type unprovability is separate from logical independence, and indeed much harder to make lists of.

My earlier point is not that we could know for sure that our struggles are due to being up against such a wall--just that our ability to suspect as much is relevant to how we allocate our time.

Oh, such as a list of statements unprovable under a specific Godel numbering? Definitely much more difficult - I never saw such a list in grad school, although I wouldn't rule out the existence of one.

> Godel-type unprovability is separate from logical independence

What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard meaning of "logical independence".

> true but unprovable under the axioms xyz?

Careful: we don't really talk about things which are "true but unprovable" in first-order logics.

By Goedel's completeness theorem, if a statement is true in all models of a first-order theory then it is provable. For any recursively axiomisable first-order theory of sufficient complexity, there exists some sentence which isn't provable [Goedel's First Incompleteness Theorem]: by contraposition of completeness, there exist models of the theory where the sentence is true, and models where the sentence is false.

So when you say "true but unprovable", you're probably talking about truth in the so-called "intended model": if something is independent of the first-order system (e.g. ZF) you're using as a foundation of mathematics, then you get to decide whether it's true or not! Once you've proven independence via e.g. forcing, it's up to you to decide whether the sentence should hold in your intended model: then you can add the appropriate axiom to your system.

Choice is independent from ZF: most mathematicians are OK with choice, so they chose to work in ZFC, but some aren't. Neither is "more valid" or "more true" from a purely logical perspective.

That's simply not true. The kinds of statements that are unprovable aren't "intuitive". Gödel provided an algorithm for creating them!

But there's no reason to believe that his algorithm gives us all of them.

Nobody has proven, for instance, that the Goldbach conjecture is unprovable, but the collective intuition of the community of number theorists is such that nobody spends much time trying to prove it anymore.

What, aside from some coded-in GIT awareness-would lead an automated prover to do the same?

Why can't an automated prover have intuition?

Today's automated provers don't, but then not so many years ago the successful computer chess players were all these boring rules-based brute force engines. And then DeepMind showed that a very different approach is better.

One could argue human intuition is just statistical sampling.

In effect, we might not be able to prove something, but we've observed that when used "assumed to be true" in other contexts, it seems to yield our expected result.

I don't see why we couldn't build a similar system of intuition into a computer as well.

> One could argue human intuition is just statistical sampling.

Human intuition lets us walk and drive cars. It has proven really hard to replicate using computers. I really doubt we will solve this any time soon.

Human intuition can also add small numbers and recognize faces, and computers can do those already. Computers replicating all of human intuition is not a prerequisite for computers beating one aspect of human intuition.

True. Yet humans are embodied beings in a physical world. This affects their mathematical taste in at least two ways. Humans will prefer axiomatic systems / problem spaces that have some bearing onto the physical world. Humans will also prefer axiomatic systems / problem spaces that have some match to their sensorial systems, and the sensorial systems are shaped by the physical world.

That being said, we are not too far from embodied computers, coming online soon as autonomous cars and autonomous killer drones. While this will not immediately give raise to physical biases in computer mathematicians, computers will become, for all intents and purposes, subject to the same physical reality which shapes humans.

You are describing (some of) physics, not math. Most of math is already far beyond human physical senses, and theoretical physics largely is too.

It's all still based on intuitive concepts like "sets" and "integers." Furthermore, inference rules are all based on the ones we use every day. You could have "alien logic" if you wanted but nobody seems to be very interested.

Of course this has no bearing on computer proofs because you can tell the computer what your preferences are.

This is a good time to illustrate that you can prove SOME programs can terminate. The halting problem doesn't limit you in proving that the following loop will halt or not:

for x in range(0,10): x = x + 1

Microsoft research even had(has?) a program that attempts to prove functions that halt and they called in the Terminator. See https://cstheory.stackexchange.com/questions/39932/practical...

NP completeness seems much more relavent than GIT to me (still not really fully relavent. The question is can computers rivial humans, not can they prove all provable theorems in reasonable time, since clearly humans cant do that)

"If computer scientists are ever able to program a kind of synthetic intuition, he says, it still won’t rival that of humans. "

Famous last words, rather similar to the initial comments made by Lee Sedol before starting his famous game against AlphaGo.

I don't think machine will ever replace mathematicians. However, I'm ready to bet that most Mathematicians in the coming 50 years who discovers anything useful will do so with CAM (computer assisted math) tools, in the same way no one designs any kind of building in 2020 without the help of a computer.

"If computer scientists are ever able to program a kind of synthetic knitting machine, he says, it still won’t rival that of humans. "

If computer scientists are ever able to program a kind of running, he says, it still won’t rival that of humans. "

It's amazing to see an "expert" saying these things unironically.

The only thing impossible for a computer to event rival a human at are things that are judged subjectively by humans. And even in they, computers are winning. Youth today are learning their culture from computer programs and bots, ever more preferring algorithmically or mechanically generated content to real humans.

So all the important things?

As a human, i care mostly about the things that i subjectively judge good. Pretty much by definition.

Your assessment seems fair to me. Computers and humans aren't in a fight to win at something, they can just reinforce the lacks of the other. What might happen is that we gradually engineer a smaller and smaller comparative gap between computers and humans by ingesting "human-stuff", and thus make it seem like humans become proportionally irrelevant in the system.

But after AlphaGo beat the best players at the game, did people entirely stop playing it? No, in fact they started analyzing the moves and trying to extract ways to improve themselves too. And people around the world don't seem to have particularly given up playing Go either. Similarly with Chess, nobody's even thinking for a second that a computer couldn't beat Magnus consistently, yet we didn't throw our hands in the air and move on from Chess altogether.

Maths is not just this abstract thing that some people do, it's something people actively enjoy. If we get computers to stump everyone by bringing something forward that "works" yet we can't grasp, it will only spark more interest in the field. Not everyone is willing to adapt to that attitude if they don't have it yet though.

Um, they have moved on from chess. The problem is you are only looking at the highly skilled people. Go look at everyone else, and you'll see chess is pretty much an expert's sport now. Casuals are more or less gone from modern life.

It’s doing pretty well as a spectator’s sport. Look at Hikaru Nakamura’s stream on a typical night. Thousands of viewers. He recently joined a major esports team (TSM). His finals match against Magnus Carlsen was up over 30k viewers at some points.

Now how many of those viewers play chess themselves? Quite a few, I think. Chess.com and Lichess are booming. Tons of low rated players playing all the time.

Another big, emerging phenomenon is Pogchamps, an online invitational chess tournament featuring top streamers of other games. These streamers tend to be very low rated in chess and they receive coaching from IMs and GMs such as the aforementioned Hikaru. In addition to the excitement around the tournament itself, a lot of people tune in to watch their favourite streamers get coached by the pros. It can be very entertaining to see a normally cocky streamer get humbled in chess.

Math is and has always been a form of expressive art, but there's been a vocal constituency since at least the early 20c that claims it's bloodless symbol manipulation. Since computers excel at bloodless symbol manipulation, one would expect them to be programmable to generate proofs of propositions; this is uninteresting to mathematicians unless it has some artistic merit.

This is a take that I generally agree with. To be honest, I kinda feel the same way about breathless think-pieces talking about GPT-3.

Many mathematicians would disagree with the claim that automated proof checking/generation (see COQ & this presentation by Voevodsky: https://www.ias.edu/ideas/2014/voevodsky-origins) and involved techniques (see the entire field of sat & smt solvers) are "uninteresting & without artistic merit".

Good thing I never claimed that, I just said it was uninteresting to mathematicians unless it has artistic merit!

Definitions and theorems to prove are (in some sense) more interesting than the proof of a given theorem.

Yes, I agree. As a mathematician, I spend lots of time trying to find the correct definitions with only a rough idea what I'm trying to prove (the theorem).

Conversely, in theoretical cs, there are many longstanding open problems. People who make progress on these problems are taken seriously and listened to precisely because they have new techniques and novel approaches that have not been considered previously - i.e. the theorems & definitions are well understood, but the proofs are the significant element.

I think mathematics is an art as well as a science. For mathematicians it can be very exciting to explore, create, and discover new mathematics and, I think, computers provide a new tool in that exploration.

So even though a camera can, for example, create a perfect representation of a sunset, that doesn’t mean paintings are now worthless.

Creating a painting of a sunset is more than just reproducing the sunset. In a similar way mathematics is more than just producing a proof.

Further, the camera is a now a whole new adventure from an artistic perspective because it is a new mechanism for creating art.

Similarly computerized systems provide a whole new adventure in terms of exploring and understanding mathematics.

Just as the classic art of creating paintings doesn’t invalidate photography, and photography doesn’t invalidate creating paintings (they are both exciting ways to make art), computerized math systems and classical math are exciting ways that can work together to discover mathematics.

“They’re very controversial for mathematicians,” DeDeo said. “Most of them don’t like the idea.”

I've always found this attitude very weird. If I was a miner, I'd welcome the arrival of a machine that helps me dig faster.

Even if I was an artist, musician, painter or otherwise working in a "creative" field, I would welcome any kind of tool that helps liberate me from the tedium of material things related to my craft and allow me to reach out further and wider.

I think there's a category of Mathematicians that still believe that their craft is something special, and that the help of machines will somehow taint the "purity" of the work. What a sad and arrogant thing to believe.

The article touches on it a little bit, but I think the main reason mathematicians are hesitant to accept the value of machines is that although they generate a "proof" in the technical sense, they usually don't generate "understanding", which is really the currency of mathematicians. What good is a proof if literally no human being can understand it? It won't lead to any new mathematics, or new conjectures to think about etc.

> What good is a proof if literally no human being can understand it?

It establishes the universal truth of a statement. So we absolutely do learn something. Until you have a proof, the statement might also be false.

Just knowing something is true without knowing why is a lot less helpful in figuring out what else is true.

You are right that computer generated proofs are often tough to understand, and that understanding is often the intended goal of writing a proof. But proofs can be useful for reasons besides human understanding, especially so in engineering. For example, when a browser establishes a secure session with an encryption protocol, the reason it is secure has to do with the difficulty of finding a proof that eg certain numbers factor, but no human cares about this proof. As another example, a compiler can use a proof that a program is type correct to optimize it, but humans would not find such proofs interesting at all.

That's great, but not relevant to mathematicians doing their jobs.

Knowing which conjectures were true would probably help mathematicians work more efficiently. At the very least nobody would spend time searching for counterexamples to true conjectures.

Existence proofs remain popular however, as do establishing upper or lower bounds.

Things immediately spring to mind:

1. What good is a proof if you don't understand it. My answer: it is super useful. You now know something is true. You may not understand why it is true, but you can use it and build on it. For example, if I write a piece of code that relies on an impossible to understand proof generated by a machine and gain a x1000 speedup with a guarantee that my shortcut will always work, there's a ton of value in there. But the utility argument is rarely something that resonates with Mathematician, they usually leave these disgustingly material details to others.

2. The modern "proofs" of important theorems, albeit produced by humans, are equivalently impossible to understand to the vast majority of Mathematicians. Mochizuki's Inter-universal Teichmüller theory is an extreme example of this (exactly one person on the planet understands the proof, assuming he's not a full-blown charlatan), but it's the same deal in other sub-fields of Maths. Can you claim to be able to explain/understand the classification of finite groups? The proof is so large and assembled by so many people it basically takes investing one's entire career to come to grasp with it.

3. It won't lead to new mathematics. I don't think it's true, for two reasons: a) who's to say the machines won't invent new mathematics. 2) falling back on humans, once you know something is true, even if you don't understand why, it's like a guiding lightbeam in a dark forest and there's a very good chance that knowing something is true will lead to a simpler, human-graspable proof.

There's is a very strong reek of stakhanovism [1] that emanates from the whole "math against the machine stance", it's just sad.

[1] https://en.wikipedia.org/wiki/Alexey_Stakhanov

[EDIT]: an one more thing : what is this "understanding" you speak of? that's a rather fuzzily defined concept. One way to codify "understanding" is to make something graspable by a human mind, by - sort of - compressing/reducing it to things that are already known/grasped. But then, there's a very good chance that some things just won't lend themselves to such treatment (incompressible if you will, such as theorem whose minimal proof just won't fit in a human mind). I'd still like to know that they're true.

Try to actually formalize some math. Just definitions and constructions without proofs. See the challenge for yourself. You might gain some different perspective and sympathy for the mathematicians you are ridiculing. Consider this question: how do you know the string of symbols you wrote down actually correspond to the mathematical objects in my head? Conversely, Voevodsky advocated that mathematicians should formalize their reasoning to flush out the subtle bugs from differences in understanding. But representing mathematical concepts is a huge challenge.

Fair points, but you are minimizing the important detail that mathematics is also a social activity, and so any argument about what constitutes mathematics should be viewed with that in mind. Mathematicians are interested in math because they want to understand things (meaning they can construct abstractions and develop logical lines of reasoning that fit within the limits of human cognition), so that they can develop new concepts and utilize existing ones in novel ways. Using a computer to prove a theorem allows you to add to the ledger of "things that are true" (which certainly has value, like you mention), but unless the proof is understandable, you don't harvest any of the other fruit that would normally come over the course of proving the theorem "the natural way" (new abstractions to ponder, new conjectures etc). I would argue that Mochizuki's "proof" occupies the same territory as a 100 GB formal logic proof generated by a computer, if the end result is that the proof is not communicable in a way that other mathematicians can relate to.

I'm not against creating machine generated proofs. We just shouldn't pretend they have the same status within "mathematics as a social construct" that a human written proof does.

Suppose there was a machine that was a black box where you could ask it whether a result was true or false, and it spit out a truth certificate that was not humanly understandable, but it could be mechanically verified.

I would find this incredibly disappointing. The appeal of mathematics is not just that I know things are true -- I know why they're true. I know why x + y = y + x, why there are infinitely many primes, why the derivative of x^2 is 2*x. Working out a proof isn't tedium -- it's the point.

What you say my be true in your corner of the world. I'm going to go on a limb and say you've not done or used much applied math in your work.

For the rest of humanity, those who build things using maths and have deadlines to meet to deliver working thins, knowing something is true for sure has incredible utility.

Understanding why it is true is most certainly nice, but it's just the icing on the cake: they have bigger fishes to fry.

Your need for utility will mostly likely be met by a symbolic algebra system not a formal reasoning system.

I'm actually an applied mathematician, so no.

You don't want to understand things? You don't care at all? All that matters to you is making that better widget? Meet that deadline?

I think having a tool but not being able to know how it works can be both amazing and frustrating at the same time (depending on the perspective of someone using the tool vs someone wanting to make the tool better).

Both perspectives are equally valid.

As a concrete example, suppose an alien cube suddenly appeared on Earth that, with a push of a button, would emit a pill.

It was discovered that the pill could cure half (but only half) of all known forms of cancer.

However, no matter how hard anyone tried, it was impossible to understand how the cube or the pill it created worked.

For those with cancer that took the pill and were cured, the cube was an amazing magical device.

For the people that took the pill and it didn't help them, the cube was worthless, since doctors couldn't tell them anything about why it didn't work, or what they could do to make it work.

For researchers it was frustrating because the cube showed some cancers are curable, but gave no reason why.

For the cancers it did cure, they didn't know why, and for those it didn't cure they also didn't know why.

Further it gave no insight into why only half were curable.

Was it because the cube was imperfect, or was that really the best that could be achieved?

For all intents and purposes, cancer research and treatment didn't really change. If you had cancer, you tried the magic pill. If it worked great. If it didn't, then doctor's were back to traditional techniques.

Thus from a knowledge perspective of one day curing all cancer, the cube didn't help, because the knowledge of how it worked couldn't be expanded to cure all cancer.

For someone cured by the cube, it was an amazing device, and nothing could change their mind.

For a cancer researcher, the cube was useless, and the only thing that could change their mind was if its mechanisms could be understood.

It is similar for math. As a tool, it is good enough to just know that the theorem is valid.

However, if you want to expand on that tool, develop more tools, or create different ways of looking at the problem, you need to understand why the theorem is true.

Please keep personal swipes out of your comments here. They're against the rules (https://news.ycombinator.com/newsguidelines.html). We've had to ask you this before.

I have no idea why you would find the existence of this machine disappointing. If you wanted to work out something for yourself then you still can.

It's a bit more complicated, and the facile 'luddite' retort doesn't help.

Humans need something to do. In times immemorial, something to do entails running around the savanna looking for edible scraps, collecting them, bringing them home and raising the next generation to repeat the process. A perfect machine that produces and delivers edible scraps with zero human effort required leaves actual humans with nothing to do. Having nothing to do is spiritually unsustainable. There is so much leisure or travel. There is so much make-believe work. After a while though, people will need something meaningful to do, something that undeniably pushes the inexorable wall of unbeing a bit further.

This is exacerbated by social effects. We confer value to other people by their ability to provide meaningful work. Assuming a perfect machine that does all the meaningful work, there is zero reason to confer value to any other human being. This is a recipe for disaster, and will hit us much sooner than the angst of nothing to do.

Imagine that careful examination of the mineshaft helps determine where the most profitable place to dig next might be... And then imagine a machine that only produced mine shafts that tell you nothing.

Sometimes the machine might be very useful! It would allow scaling up solutions for downstream users. For example, if you have more people who want solutions to many slightly-different complicated integrals that we don't have a good overarching theory to solve.

But in other cases, knowing /where/ to dig is much more important than how fast you dig.

If you were a miner, that tool that helps you dig faster would put you out of a job, because now they only need half the miners to do the same amount of work.

If you were an artist, a lot of the point is the material things, or the process. Why on earth use oil paint than instead of Photoshop or other digital tools? Why do people use paper at all? It's so inefficient. But art really is personal and inefficient most of the time.

> arrival of a machine that helps me dig faster

This is usually wrong for the current SotA of ITPs.

One important difference between verified programs (that the article mentions is useful) and mathematical results is that the former usually involves properties that are very complicated to state with many moving parts, but are usually straightforward to prove. On the other hand, mathematical results usually have a straightforward central concept, and the complicated details (if there are) can be altered to slightly change the result.

To the mathematician, these complicated details are understood to be nonessential to the result and can be omitted, or reduced to a a comment or reference. And if the theorem is wrong, it can usually be salvaged.

But with provers, you are forced to get bogged down in the details.

The analogy to mining machines is wrong; the appropriate comparison is something more like writing in Python vs. writing in assembly. Writing in assembly you have a better guarantee that the computer is behaving exactly as you told it to.

But it's less portable (e.g. you must decide to encode tuples primarily as a product, or as a finite sequence, one of many nonessential decisions that are important to a prover), just as asm is less portable than a python program. You have to get bogged down in details that you can make errors in that you don't in Python; (respectively, informal proof). It's harder for peers to understand the thrust of what is happening. etc.

It's irresponsible to not mention that a series of results from the 1930s through the 1950s proved that generalized automated proof search is impossible, in the sense that 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. In that sense, no, computers will never fully automate mathematical reasoning, because mathematical reasoning cannot be fully automated.

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

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

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

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

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.

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.

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

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"?

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.

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.

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.

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

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

Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have it walk down the tree of proof possibilities (possibly using Q-learning), trim incorrect branches, and then out comes a proof. Somewhere in its modestly coherent glossolalia, GPT3 will figure out how to prove something "tough for humans" correct. Nice thing is, you might even be able to paralellize the search using independent agents.

Is there anyone working on this? Drop a line.

I ran some experiments with GPT3+proofs. You can read about it here: http://serendipityrecs.com/blog/posts/experiments-with-gpt-3... I wasn't able to get it to return anything interesting but I also didn't spend a lot of time refining the approach (this was just a series of quick and dirty experiments, ultimately I identified recommendations as a good use case for GPT-3 and started building a product around it.)

I think it will be interesting to use GPT-3 in conjunction with existing automated/machine proof techniques. Since GPT-3 doesn't "know" anything, automated proof systems can help the system stay logically consistent.

GPT-3 is approximate remixes of old text. How is that at all relevant to theorem proving, which is a search problem?

Any proof is also a remix of old text (and often times old ideas too)

Reply on news.ycombinator.com