5 ms·

My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.

by brap 3y ago

prmph 3y ago
I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.
- dumbo-octopus 3y ago
  In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
  - gpm 3y ago
    def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
    - brap 3y ago
      >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted
    - dumbo-octopus 3y ago
      Clearly the prevalence of idk's in the output is the metric for determining power. As for the human-vs-computer, I think the most powerful solutions will be those that combine human and computer prowess, similar to how a Human+Stockfish beats Stockfish^. To that end I've been working on Lean search tools that keep a human firmly in the loop. Terence has actually called out a tool I helped make as being quite helpful in his work, which is rather neat. ^ I heard this to be true at some point, but cannot find any reference on it at the moment.
      - gpm 3y ago
        > similar to how a Human+Stockfish beats Stockfish^ > ^ I heard this to be true at some point, but cannot find any reference on it at the moment. Known as centaur chess (amongst other things). It was certainly the case at one point. I strongly suspect that it isn't still the case, but it's hard to say for absolute certainty because it never developed a serious competitive community like engine and non-engine chess has. I can't find anyone listing any results post 2017 [1]. It was barely the case in 2017, and Stockfish has improved a lot since then [2]. [1] https://gwern.net/note/note#advanced-chess-obituary https://gwern.net/note/note#advanced-chess-obituary [2] E.g. here's someone running stockfish 14 (current from July 2 2021 - April 18 2022) against stockfish 8 (current from November 1 2016 to February 1 2018). Stockfish 14 won 61 games and drew 3: https://www.reddit.com/r/chess/comments/oov714/64_game_match_between_the_new_stockfish_14_and/ https://www.reddit.com/r/chess/comments/oov714/64_game_match... (PS: They don't document time controls and I'm not sure how scientific this test was, but it matches with what I would expect, so eh) Not to discourage you from your project with lean. At the very least I would expect there to be a transitional period, likely of decades, where computer+human is better than computer.
        zone411 3y ago
        In the 2022 Correspondence Chess Championship, humans hurt the performance of computers by themselves. I posted about this here: https://twitter.com/LechMazur/status/1721008768899555677 https://twitter.com/LechMazur/status/1721008768899555677
  - thaumasiotes 3y ago
    > "antiProof: ..." The standard terminology would be "counterexample".
- dellamonica 3y ago
  It doesn't require anything like that. Math proofs are of NP complexity. If you had access to a non deterministic Turing machine you could enumerate all possible proofs of a given length and check them all in poly time. That does not say anything about LLMs though. Personally, I believe they could be quite helpful to mathematicians in a way similar to copilot for software programming.
  - explaininjs 3y ago
    > you could enumerate all possible proofs of a given length That does not help us with proof search as we do not know the target length.
    - bawolff 3y ago
      A proof longer than the size of the universe is also pretty useless and probably not something we need to worry about. Like i guess you are saying we couldn't really use such a machine to determine whether a certain conjecture just has a very long proof/disproof or is actually undecidable. Which sure, but umm i think that is the sort of problem most mathematicians would love to have. The real reason non-deterministic turing machines can't help us is that they dont actually exist.
    - dellamonica 3y ago
      Of course it would, you would enumerate lengths too. If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.
      - explaininjs 3y ago
        > If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway. We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.
        3y ago
- deleted 3y ago
  [deleted]
  - Ar-Curunir 3y ago
    Given that algorithm design is very much a field of mathematics, it’s in principle (and probably in practice) not too difficult to adapt the infrastructure you mentioned to support a workflow where you say “I want an algorithm that on input x computes y” (more formally, ofc), and the tool outputs exactly that for you
waynecochran 3y ago
Neither RH nor P vs NP will succumb.

My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.

by brap 3y ago

My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.

prmph 3y ago

I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.

dumbo-octopus 3y ago
In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
- gpm 3y ago
  def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
  - brap 3y ago
    >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted
  - dumbo-octopus 3y ago
    Clearly the prevalence of idk's in the output is the metric for determining power. As for the human-vs-computer, I think the most powerful solutions will be those that combine human and computer prowess, similar to how a Human+Stockfish beats Stockfish^. To that end I've been working on Lean search tools that keep a human firmly in the loop. Terence has actually called out a tool I helped make as being quite helpful in his work, which is rather neat. ^ I heard this to be true at some point, but cannot find any reference on it at the moment.
    - gpm 3y ago
      > similar to how a Human+Stockfish beats Stockfish^ > ^ I heard this to be true at some point, but cannot find any reference on it at the moment. Known as centaur chess (amongst other things). It was certainly the case at one point. I strongly suspect that it isn't still the case, but it's hard to say for absolute certainty because it never developed a serious competitive community like engine and non-engine chess has. I can't find anyone listing any results post 2017 [1]. It was barely the case in 2017, and Stockfish has improved a lot since then [2]. [1] https://gwern.net/note/note#advanced-chess-obituary https://gwern.net/note/note#advanced-chess-obituary [2] E.g. here's someone running stockfish 14 (current from July 2 2021 - April 18 2022) against stockfish 8 (current from November 1 2016 to February 1 2018). Stockfish 14 won 61 games and drew 3: https://www.reddit.com/r/chess/comments/oov714/64_game_match_between_the_new_stockfish_14_and/ https://www.reddit.com/r/chess/comments/oov714/64_game_match... (PS: They don't document time controls and I'm not sure how scientific this test was, but it matches with what I would expect, so eh) Not to discourage you from your project with lean. At the very least I would expect there to be a transitional period, likely of decades, where computer+human is better than computer.
      - zone411 3y ago
        In the 2022 Correspondence Chess Championship, humans hurt the performance of computers by themselves. I posted about this here: https://twitter.com/LechMazur/status/1721008768899555677 https://twitter.com/LechMazur/status/1721008768899555677
- thaumasiotes 3y ago
  > "antiProof: ..." The standard terminology would be "counterexample".
dellamonica 3y ago
It doesn't require anything like that. Math proofs are of NP complexity. If you had access to a non deterministic Turing machine you could enumerate all possible proofs of a given length and check them all in poly time. That does not say anything about LLMs though. Personally, I believe they could be quite helpful to mathematicians in a way similar to copilot for software programming.
- explaininjs 3y ago
  > you could enumerate all possible proofs of a given length That does not help us with proof search as we do not know the target length.
  - bawolff 3y ago
    A proof longer than the size of the universe is also pretty useless and probably not something we need to worry about. Like i guess you are saying we couldn't really use such a machine to determine whether a certain conjecture just has a very long proof/disproof or is actually undecidable. Which sure, but umm i think that is the sort of problem most mathematicians would love to have. The real reason non-deterministic turing machines can't help us is that they dont actually exist.
  - dellamonica 3y ago
    Of course it would, you would enumerate lengths too. If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway.
    - explaininjs 3y ago
      > If the lengths need to be larger than polynomially bounded then we can be sure it would never be found by a human anyway. We cannot, as a human might be able to intuitively devise proof that might be quite large in the target language but easily constructible in a separate one.
      - 3y ago
deleted 3y ago
[deleted]
- Ar-Curunir 3y ago
  Given that algorithm design is very much a field of mathematics, it’s in principle (and probably in practice) not too difficult to adapt the infrastructure you mentioned to support a workflow where you say “I want an algorithm that on input x computes y” (more formally, ofc), and the tool outputs exactly that for you

waynecochran 3y ago

Neither RH nor P vs NP will succumb.