5 ms·

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify the correctness. One hallucination in 300 steps of logic is enough to destroy the entire proof.

skipkey 4mo ago
I would imagine that in the future AI will be doing proofs in Lean or whatever the successor to it, which gives you a pretty good confidence it’s correct.
- bckgrndrdtn 4mo ago
  The future is now. See the article under discussion for some examples.
jonahx 4mo ago
> It would be great if someone could explain to me how AI improves this situation. It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean. > One hallucination in 300 steps of logic is enough to destroy the entire proof. The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.
- tacomonstrous 4mo ago
  >The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired. In fact, it was Wiles himself who realized there was an error.
  - jonahx 4mo ago
    Yes, at the prodding of the reviewer (from wikipedia): > After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap. It seems likely Katz played a crucial role here. Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.
hilbertseries 4mo ago
In 2012 Mochizuki claimed to have proved the abc conjecture by developing a new branch of mathematics. He was a respected mathematician, but the theories he had developed were so complex no one could determine if he was correct. It took six years until two number theorists dissected the proof and found a fatal flaw in it.
- scheme271 4mo ago
  Mochizuki and a group of mathematicians still claim that Stix and Scholze didn't actually identify a flaw and his proof was published in a journal (where Mochizuki is the chief editor and the reviewers were people from Mochizuki's instituion). I think most of the math community don't believe his proof although Mochizuki and some others claim it's valid.
deleted 4mo ago
[deleted]
jstanley 4mo ago
This is what Lean is for: https://lean-lang.org/ https://lean-lang.org/ If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).
- AaronAPU 4mo ago
  I’m playing devil’s advocate here, so go easy on me. But how completely do we know lean is perfectly true in all cases?
  - bckgrndrdtn 4mo ago
    There's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/ https://lean-lang.org/doc/reference/latest/ValidatingProofs/ But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".
  - pfdietz 4mo ago
    If there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times. It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.
throw310822 4mo ago
> even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. I hope mathematicians have the self-respect of not establishing rules such as "if a proof is longer than X, break it up in smaller ones, otherwise it'll be outright rejected".

skipkey 4mo ago

I would imagine that in the future AI will be doing proofs in Lean or whatever the successor to it, which gives you a pretty good confidence it’s correct.

bckgrndrdtn 4mo ago
The future is now. See the article under discussion for some examples.

jonahx 4mo ago

> It would be great if someone could explain to me how AI improves this situation. It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean. > One hallucination in 300 steps of logic is enough to destroy the entire proof. The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.

tacomonstrous 4mo ago
>The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired. In fact, it was Wiles himself who realized there was an error.
- jonahx 4mo ago
  Yes, at the prodding of the reviewer (from wikipedia): > After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap. It seems likely Katz played a crucial role here. Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.

hilbertseries 4mo ago

In 2012 Mochizuki claimed to have proved the abc conjecture by developing a new branch of mathematics. He was a respected mathematician, but the theories he had developed were so complex no one could determine if he was correct. It took six years until two number theorists dissected the proof and found a fatal flaw in it.

scheme271 4mo ago
Mochizuki and a group of mathematicians still claim that Stix and Scholze didn't actually identify a flaw and his proof was published in a journal (where Mochizuki is the chief editor and the reviewers were people from Mochizuki's instituion). I think most of the math community don't believe his proof although Mochizuki and some others claim it's valid.

deleted 4mo ago

[deleted]

jstanley 4mo ago

This is what Lean is for: https://lean-lang.org/ https://lean-lang.org/ If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).

AaronAPU 4mo ago
I’m playing devil’s advocate here, so go easy on me. But how completely do we know lean is perfectly true in all cases?
- bckgrndrdtn 4mo ago
  There's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/ https://lean-lang.org/doc/reference/latest/ValidatingProofs/ But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".
- pfdietz 4mo ago
  If there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times. It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.

throw310822 4mo ago

> even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. I hope mathematicians have the self-respect of not establishing rules such as "if a proof is longer than X, break it up in smaller ones, otherwise it'll be outright rejected".