6 ms·

One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. Generally, most computer scientists u

One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. Generally, most computer scientists using proof automation don't care about the proof itself -- they care that one exists. It can contain as many lemmas and steps as needed. They're unlikely to ever read it. It seems to me that LLMs would be decent at generating proofs this way: so long as they submit their tactics to the proof checker and the proof is found they can generate whatever is needed. However for mathematicians, of which I am not a member of that distinguished group, seem to appreciate qualities in proofs such as elegance and simplicity. Many mathematicians that I've heard respond to the initial question believe that a proof generated by some future AI system will not be useful to humans if they cannot understand and appreciate it. The existence of a proof is not enough. Now that we're getting close to having algorithms that can generate proofs it makes the question a bit more urgent, I think. What use is a proof that isn't elegant? Are proofs written for a particular audience or are they written for the result?

Davidbrcz 2y ago
It depends. A proven conjecture is IMO better than an unproven one. But usually, a new proof would shed new lights or build bridges between concepts that were before unrelated. And in that sense, a proof not understandable by humans is disappointing, because it doesn't really fullfil the need to understand the reason behind why it's true.
crabbone 2y ago
This isn't a new conundrum. This was a very contentious question in the end of the 19th century, where French mathematicians clashed with the German mathematicians. Poincare is known for describing proofs as texts intended to convince other mathematicians that something is the case, whereas Hilbert believed that automation is the way to go (i.e. have a "proof machine", plug in the question, get the answer and be done with it). Temporarily, Germans won. Personally, I don't think that proofs that cannot be understood have no value. We rely on such proofs all the time in our day-to-day interpretation of the world around us, our ability to navigate it and anticipate it. I.e. there's some sort of an automated proof tool in our brains that takes the visual input, feeling of muscle tonus, feeling of the force exerted on our body etc. and then gives an answer as to whether we are able to take the next step, pick up a rock and so on. But, mathematicians also want proofs to be useful to explain the nature of the thing in question. Because another thing we want to do about things like picking up rocks, is we want to make that more efficient, make inanimate systems that can pick up rocks etc. ---- NB. I'm not entirely sure how much LLMs can contribute in this field. The first successes of AI were precisely in the field of automated proofs, and that's where symbolic AI seems to work great. But, I'm not at all an expert on LLMs. Maybe there's some way I cannot think about that they would be better at this task, but on the face of it they just aren't.
- rocqua 2y ago
  From what I have heard when talking to the people behind formal analysis of protocol security, the main problem currently with using LLMs to 'interact with the theorem prover for you' is that there is nowhere near enough proofs out there for the LLMs to learn how to generalize from them.
chii 2y ago
i would imagine a proof has several "uses": 1) the proof itself is useful for some other result or proof, and 2), the proof is using a novel technique or uses novel maths, or links to previously unlinked fields, and it's not the proof's result itself that is useful, but the technique developed. This technique can then be applied in other areas to produce other kinds of proofs or knowledge. I suspect it is the latter that will suffer in automated proofs perhaps - without understanding the techniques, or if the technique is not really novel but just tedious.
knappa 2y ago
Mathematician here (trained as pure, working as applied). Non-elegant proofs are useful, if the result is important. e.g. People would still be excited by an ugly proof of the Riemann hypothesis.^1 It's important too a lot of other theorems if this is true or not. However, if the result is less central you won't get a lot of interest. Part of it is, I think, that "elegance" is flowery language that hides what mathematicians really want: not so much new proofs as new proof techniques and frameworks. An "elegant" proof can, with some modification, prove a lot more than its literal statement. That way, even if you don't care much about the specific result, you may still be interested because it can be altered to solve a problem you _were_ interested in. 1: It doesn't have to be as big of a deal as this.
- The_suffocated 2y ago
  "It doesn't have to be as big of a deal as this." Agree. The truthfulness of the four-colour theorem is good to know, although there is not yet any human-readable proof.
  - rocqua 2y ago
    I feel like the four-color theorem automated proof is much more 'human-readable' than the proofs done with automated theorem provers. Because with the four-color theorem, there is a human readable proof that says "if this finite set of cases are all colorable, then all planar graphs are colorable". And then there is some rather concrete code that generates all the finite cases, and finds a coloring for them. Every step in there makes sense, and is fully understandable. The fact that the exhaustive checking wasn't done by hand doesn't mean its hard to understand how the proof works, or what is 'actually going on'. For a general theorem prover, reading the code doesn't explain anything insightful about why the theorem is true. For the 4 color theorem, the code that proved it actually gives insight in how the proof works.
- LegionMammal978 2y ago
  Then again, even an 'elegant' proof can be surprisingly inflexible. I've recently been working through Apéry's proof that ζ(3) is irrational. It's so simple that even a clueless dabbler like me can understand all the details. Yet no one has been able to make his construction work directly for anything else (that hasn't already been proven irrational). C'est la vie, I suppose.
QuesnayJr 2y ago
I think mathematicians want something more basic, though elegance and simplicity are appreciated. They want to know why something is true, in a way that they can understand. People will write new proof of existing results if they think they get at the "why" better, or even collect multiple proofs of the same result if they each get at the "why" in different ways.
- agentultra 2y ago
  In my limited experience it seems like the "why" of a proof requires a theory of mind from the perspective of the author of the proof. What I mean is that one could choose a particular tactic to proving a lemma or even rely on certain lemma where that choice is intended for the audience the author has in mind in order to help them understand the steps better. The context an LLM uses is limited (though growing). However its context is lacking the ability to understand the mind of the interlocutor and the proof they would expect or find helpful. "Why this proof?" also has a more global context as well. It seems there are have been styles and shifts in cultural norms over the years in proofs. Even though the Elements stood up until the 19th century we don't necessarily write proofs in the style of Euclid even though we may refer to those themes and styles, on purpose, in order to communicate a subtle point.
  - daxfohl 2y ago
    Though, say we finally solve chess. There's not always going to be a "why" the suggested move is the best. There might be heuristics, or even some set of rules in the end game or certain situations that a human's brain can retain to perfection. But for the vast majority of the game, the correct move is what it is, because that's what the computer says, and there's not much more you can do to simplify it. Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.
flatline 2y ago
Hypothesis: an LLM capable of generating a correct proof in a formal language, not through random chance but through whatever passes for “reasoning,” should also be capable of describing the proof in a way meaningful to humans. Because LLMs have a limited context window and are trained on human behavior, they will generate solutions similar to what humans would generate. We have already accepted some proofs we cannot fully understand, such as the proof of the four color theorem that used computational methods to explore a large solution space and demonstrate that no possible special-case combinations violate the theorem. But that was just one part of the proof. I wonder what we know about proof space generally, and if we had an ASI that reasoned in a substantially different way than humans, what types of proofs it would be likely to generate. Do most proofs contain structural components that humans find pleasing? Do most devolve into convoluted case analyses? Is there a simplest form that a set of correct proofs could be reduced to?
- ndriscoll 2y ago
  To me this seems obvious. Copilot might generate wrong things, but what I've seen tends to be human-readable. My experience with Lean is that it feels very much like a functional programming language like Scala, so I'd have to assume that a coding assistant that also knows Lean syntax/libraries would work just like any other programming language. There will perhaps need to be a transition period where we might need to look at basic type theory augmenting or replacing material in introductory proof classes. Instead of truth tables and ZFC, teach math-as-programming. Propositions are types, implications are functions, etc. If you have the right foundation, I think the stuff ends up being quite legible. Mathlib is very abstract which makes it harder to approach as a beginner, but you could imagine a sort of literate programming approach where we walk students through building their own personal Mathlib, refactoring it to use higher abstractions as they build it up, etc. In a sense this is what a math education is today, but with a kind of half-formal, half-natural language and with a bunch of implicit assumptions about what techniques the student really knows (since details are generally omitted) vs. letting them use whatever macros/tactics/theorems they've learned/created in other courses. This could all be especially powerful if the objects you're working with have good Widgets[0][1] so you could visualize and interact with various intermediate expressions. I see tons of potential here. The Lean games[2] also show the potential for a bright future here that's kind of along the lines of "build your own library around topic X" (the NN game has been posted here a few times, but it's actually a framework with other games too!). [0] https://lean-lang.org/lean4/doc/examples/widgets.lean.html https://lean-lang.org/lean4/doc/examples/widgets.lean.html [1] https://github.com/leanprover-community/ProofWidgets4/blob/main/doc/infoview-rbtree.png https://github.com/leanprover-community/ProofWidgets4/blob/m... [2] https://adam.math.hhu.de/ https://adam.math.hhu.de/
math-ias 2y ago
I believe knowing a proof exists will bring us closer to elegant human proofs. I wanted to justify this with the “Roger Bannister Effect”. The thought is that we’re held back psychologically by the idea of the impossible. It takes one person to do it. And now everyone can do it, freed from the mind trap. But further reading shows we were incrementally approaching what Roger Bannister did first: the 4 minute mile. And the pause before that record was likely not psychological but physical with World War Two. [0] And this jives with the TFA when Mr. Wolfram writes about a quarter of a century not yielding a human interpretation of his computer’s output. All I’m left with is my anecdotes. I had a math professor in college who assigned homework every class. Since it was his first time teaching, he came up with the questions live. I’d come to class red in the face after struggling with questions all night. Then the professor would sheepishly reveal some of his statements were false. That unknown sapped a lot of motivation. Dead ends felt more conclusive. Falsehood was an easy scapegoat. [0] https://www.scienceofrunning.com/2017/05/the-roger-bannister-effect-the-myth-of-the-psychological-breakthrough.html?v=47e5dceea252 https://www.scienceofrunning.com/2017/05/the-roger-bannister...
- QuesnayJr 2y ago
  I think there is something to this idea. There have been cases where person A was working on proving a result but struggled, then person B announced a proof of the result, and then person A was inspired to finish their proof. (Sadly, I don't remember the specifics.)
glenstein 2y ago
>One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. I'm skeptical of an in-principle impossibility of understanding complex proofs. I think computers likely will have, or already do have, a capability for explaining proofs piecemeal, with explanations that bridge from the proof itself to familiar intuitions. Needing to understanding by increasingly sophisticated bridge explanations may be us getting further removed from immediate understanding but I don't think it crosses a magical threshold or anything that fundamentally calls into question how operational/useful the proofs are.
youoy 2y ago
An ugly proof is super useful. It turns a statement into a theorem. There is a famous quote by Riemann: "If only I had the theorems! Then I should find the proofs easily enough. " Once you have a proof, simplifying it should be much easier, even for computers.
kolinko 2y ago
With formal verification, what you want is correct statement of invariants / things to prove. As long as these are understandable, the readibility of proof doesn't matter much - it's the program job to verify that the proof is correct.
wslh 2y ago
> One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. There are proofs created by humans that cannot be undersood by humans or for many few. For example the Fermat Last's Theorem proof.
daxfohl 2y ago
Maybe buried in that proof is the key insight needed to prove P != NP. Elegance would make it more likely that this insight is pulled out and identified.

Davidbrcz 2y ago

It depends. A proven conjecture is IMO better than an unproven one. But usually, a new proof would shed new lights or build bridges between concepts that were before unrelated. And in that sense, a proof not understandable by humans is disappointing, because it doesn't really fullfil the need to understand the reason behind why it's true.

crabbone 2y ago

This isn't a new conundrum. This was a very contentious question in the end of the 19th century, where French mathematicians clashed with the German mathematicians. Poincare is known for describing proofs as texts intended to convince other mathematicians that something is the case, whereas Hilbert believed that automation is the way to go (i.e. have a "proof machine", plug in the question, get the answer and be done with it). Temporarily, Germans won. Personally, I don't think that proofs that cannot be understood have no value. We rely on such proofs all the time in our day-to-day interpretation of the world around us, our ability to navigate it and anticipate it. I.e. there's some sort of an automated proof tool in our brains that takes the visual input, feeling of muscle tonus, feeling of the force exerted on our body etc. and then gives an answer as to whether we are able to take the next step, pick up a rock and so on. But, mathematicians also want proofs to be useful to explain the nature of the thing in question. Because another thing we want to do about things like picking up rocks, is we want to make that more efficient, make inanimate systems that can pick up rocks etc. ---- NB. I'm not entirely sure how much LLMs can contribute in this field. The first successes of AI were precisely in the field of automated proofs, and that's where symbolic AI seems to work great. But, I'm not at all an expert on LLMs. Maybe there's some way I cannot think about that they would be better at this task, but on the face of it they just aren't.

rocqua 2y ago
From what I have heard when talking to the people behind formal analysis of protocol security, the main problem currently with using LLMs to 'interact with the theorem prover for you' is that there is nowhere near enough proofs out there for the LLMs to learn how to generalize from them.

chii 2y ago

i would imagine a proof has several "uses": 1) the proof itself is useful for some other result or proof, and 2), the proof is using a novel technique or uses novel maths, or links to previously unlinked fields, and it's not the proof's result itself that is useful, but the technique developed. This technique can then be applied in other areas to produce other kinds of proofs or knowledge. I suspect it is the latter that will suffer in automated proofs perhaps - without understanding the techniques, or if the technique is not really novel but just tedious.

knappa 2y ago

Mathematician here (trained as pure, working as applied). Non-elegant proofs are useful, if the result is important. e.g. People would still be excited by an ugly proof of the Riemann hypothesis.^1 It's important too a lot of other theorems if this is true or not. However, if the result is less central you won't get a lot of interest. Part of it is, I think, that "elegance" is flowery language that hides what mathematicians really want: not so much new proofs as new proof techniques and frameworks. An "elegant" proof can, with some modification, prove a lot more than its literal statement. That way, even if you don't care much about the specific result, you may still be interested because it can be altered to solve a problem you _were_ interested in. 1: It doesn't have to be as big of a deal as this.

The_suffocated 2y ago
"It doesn't have to be as big of a deal as this." Agree. The truthfulness of the four-colour theorem is good to know, although there is not yet any human-readable proof.
- rocqua 2y ago
  I feel like the four-color theorem automated proof is much more 'human-readable' than the proofs done with automated theorem provers. Because with the four-color theorem, there is a human readable proof that says "if this finite set of cases are all colorable, then all planar graphs are colorable". And then there is some rather concrete code that generates all the finite cases, and finds a coloring for them. Every step in there makes sense, and is fully understandable. The fact that the exhaustive checking wasn't done by hand doesn't mean its hard to understand how the proof works, or what is 'actually going on'. For a general theorem prover, reading the code doesn't explain anything insightful about why the theorem is true. For the 4 color theorem, the code that proved it actually gives insight in how the proof works.
LegionMammal978 2y ago
Then again, even an 'elegant' proof can be surprisingly inflexible. I've recently been working through Apéry's proof that ζ(3) is irrational. It's so simple that even a clueless dabbler like me can understand all the details. Yet no one has been able to make his construction work directly for anything else (that hasn't already been proven irrational). C'est la vie, I suppose.

QuesnayJr 2y ago

I think mathematicians want something more basic, though elegance and simplicity are appreciated. They want to know why something is true, in a way that they can understand. People will write new proof of existing results if they think they get at the "why" better, or even collect multiple proofs of the same result if they each get at the "why" in different ways.

agentultra 2y ago
In my limited experience it seems like the "why" of a proof requires a theory of mind from the perspective of the author of the proof. What I mean is that one could choose a particular tactic to proving a lemma or even rely on certain lemma where that choice is intended for the audience the author has in mind in order to help them understand the steps better. The context an LLM uses is limited (though growing). However its context is lacking the ability to understand the mind of the interlocutor and the proof they would expect or find helpful. "Why this proof?" also has a more global context as well. It seems there are have been styles and shifts in cultural norms over the years in proofs. Even though the Elements stood up until the 19th century we don't necessarily write proofs in the style of Euclid even though we may refer to those themes and styles, on purpose, in order to communicate a subtle point.
- daxfohl 2y ago
  Though, say we finally solve chess. There's not always going to be a "why" the suggested move is the best. There might be heuristics, or even some set of rules in the end game or certain situations that a human's brain can retain to perfection. But for the vast majority of the game, the correct move is what it is, because that's what the computer says, and there's not much more you can do to simplify it. Maybe a good proof golf game would be finding the least computationally intensive proof of tic tac toe or rubics cube or something.

flatline 2y ago

Hypothesis: an LLM capable of generating a correct proof in a formal language, not through random chance but through whatever passes for “reasoning,” should also be capable of describing the proof in a way meaningful to humans. Because LLMs have a limited context window and are trained on human behavior, they will generate solutions similar to what humans would generate. We have already accepted some proofs we cannot fully understand, such as the proof of the four color theorem that used computational methods to explore a large solution space and demonstrate that no possible special-case combinations violate the theorem. But that was just one part of the proof. I wonder what we know about proof space generally, and if we had an ASI that reasoned in a substantially different way than humans, what types of proofs it would be likely to generate. Do most proofs contain structural components that humans find pleasing? Do most devolve into convoluted case analyses? Is there a simplest form that a set of correct proofs could be reduced to?

ndriscoll 2y ago
To me this seems obvious. Copilot might generate wrong things, but what I've seen tends to be human-readable. My experience with Lean is that it feels very much like a functional programming language like Scala, so I'd have to assume that a coding assistant that also knows Lean syntax/libraries would work just like any other programming language. There will perhaps need to be a transition period where we might need to look at basic type theory augmenting or replacing material in introductory proof classes. Instead of truth tables and ZFC, teach math-as-programming. Propositions are types, implications are functions, etc. If you have the right foundation, I think the stuff ends up being quite legible. Mathlib is very abstract which makes it harder to approach as a beginner, but you could imagine a sort of literate programming approach where we walk students through building their own personal Mathlib, refactoring it to use higher abstractions as they build it up, etc. In a sense this is what a math education is today, but with a kind of half-formal, half-natural language and with a bunch of implicit assumptions about what techniques the student really knows (since details are generally omitted) vs. letting them use whatever macros/tactics/theorems they've learned/created in other courses. This could all be especially powerful if the objects you're working with have good Widgets[0][1] so you could visualize and interact with various intermediate expressions. I see tons of potential here. The Lean games[2] also show the potential for a bright future here that's kind of along the lines of "build your own library around topic X" (the NN game has been posted here a few times, but it's actually a framework with other games too!). [0] https://lean-lang.org/lean4/doc/examples/widgets.lean.html https://lean-lang.org/lean4/doc/examples/widgets.lean.html [1] https://github.com/leanprover-community/ProofWidgets4/blob/main/doc/infoview-rbtree.png https://github.com/leanprover-community/ProofWidgets4/blob/m... [2] https://adam.math.hhu.de/ https://adam.math.hhu.de/

math-ias 2y ago

I believe knowing a proof exists will bring us closer to elegant human proofs. I wanted to justify this with the “Roger Bannister Effect”. The thought is that we’re held back psychologically by the idea of the impossible. It takes one person to do it. And now everyone can do it, freed from the mind trap. But further reading shows we were incrementally approaching what Roger Bannister did first: the 4 minute mile. And the pause before that record was likely not psychological but physical with World War Two. [0] And this jives with the TFA when Mr. Wolfram writes about a quarter of a century not yielding a human interpretation of his computer’s output. All I’m left with is my anecdotes. I had a math professor in college who assigned homework every class. Since it was his first time teaching, he came up with the questions live. I’d come to class red in the face after struggling with questions all night. Then the professor would sheepishly reveal some of his statements were false. That unknown sapped a lot of motivation. Dead ends felt more conclusive. Falsehood was an easy scapegoat. [0] https://www.scienceofrunning.com/2017/05/the-roger-bannister-effect-the-myth-of-the-psychological-breakthrough.html?v=47e5dceea252 https://www.scienceofrunning.com/2017/05/the-roger-bannister...

QuesnayJr 2y ago
I think there is something to this idea. There have been cases where person A was working on proving a result but struggled, then person B announced a proof of the result, and then person A was inspired to finish their proof. (Sadly, I don't remember the specifics.)

glenstein 2y ago

>One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. I'm skeptical of an in-principle impossibility of understanding complex proofs. I think computers likely will have, or already do have, a capability for explaining proofs piecemeal, with explanations that bridge from the proof itself to familiar intuitions. Needing to understanding by increasingly sophisticated bridge explanations may be us getting further removed from immediate understanding but I don't think it crosses a magical threshold or anything that fundamentally calls into question how operational/useful the proofs are.

youoy 2y ago

An ugly proof is super useful. It turns a statement into a theorem. There is a famous quote by Riemann: "If only I had the theorems! Then I should find the proofs easily enough. " Once you have a proof, simplifying it should be much easier, even for computers.

kolinko 2y ago

With formal verification, what you want is correct statement of invariants / things to prove. As long as these are understandable, the readibility of proof doesn't matter much - it's the program job to verify that the proof is correct.

wslh 2y ago

> One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans. There are proofs created by humans that cannot be undersood by humans or for many few. For example the Fermat Last's Theorem proof.

daxfohl 2y ago

Maybe buried in that proof is the key insight needed to prove P != NP. Elegance would make it more likely that this insight is pulled out and identified.