5 ms·

The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really

by kriro 1mo ago

The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really hard to explain to humans, even by GMs. They can sort of explain that something is a good line but not why. Engines crush GMs and are considered ground truth even if noone really understands what is happening. Would it be a nightmare if math was the same, not sure. Especially for counterexamples LLM solutions seem fine. They stop humans from wasting time on pointless things. For proofs it gets more hairy but I think if it is formally verified a proof is a proof. Attribution is a problem (should the person who wrangled the answer out of an LLM get the credit, I guess so). I think these are non-trivial epistemology and science theory problems.

GPerson 1mo ago
I don’t think it’s pointless to spend time trying to prove a conjecture which is ultimately false if along the way you figure out a bunch of different true variations on the conjecture, which is how mathematics actually works. This is something I’m a bit worried about with LLMs since it gets you to the end too fast.
- ianm218 1mo ago
  LLMs seem to have worse intuition than experts and compensate by being able to cover a much wider surface area of ideas, so we might just need to extract the intermediate progress along the way.
jhrmnn 1mo ago
I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?
- metahuman_crumb 1mo ago
  I suggest "Catching crumbs from the table" by Ted Chiang. Very short piece published in Nature (2000) and well worth a read. Depicts a scenario where modified humans produce science beyond ordinary scientists' comprehension.
  - cfiggers 1mo ago
    This is a theme in Blindsight by Peter Watts as well. In that setting, field experts working at the bleeding edge are so advanced that non-experts literally can't understand what they're saying at all. So there's a whole class of specialists, "synthesists", that specialize in gaining approximate understanding of the experts' work for the purpose of communicating it to outsiders—perhaps wrongly, according to the expert at least, but hopefully more productively vs the unmediated version.
    - cfiggers 1mo ago
      What's amusing to me in this context is, summarizing emails and such has for a while been a supposed use case for AI—the LLM serving as the "synthesist" to explain long texts accessibly. But with this math question, a human "synthesist" would be needed to approximately understand the math discovered and programmatically verified by the LLM. So the roles reverse.
- Jblx2 1mo ago
  Mochizuki enters the chat
  - OhNoNotAgain_99 1mo ago
    [dead]
- JadeNB 1mo ago
  Presumably there's not much logical obstruction to all human-understandable math eventually being formalized, although the willingness and ability to commit the requisite enormous amount of time will probably be insurmountable. But definitely that hasn't happened already!
RandomLensman 1mo ago
If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?
- timjver 1mo ago
  The whole point of Lean is that you don't need to understand the entire proof to be sure that it's correct. You only need to understand the definition of the theorem being proven, and you need to trust that the relatively small core of Lean is correct.
  - RandomLensman 1mo ago
    Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
    - rowanG077 1mo ago
      Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
  - gowld 1mo ago
    Why should you trust that the relatively small core of Lean is correct? The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.
  - raincole 1mo ago
    I don't think Lean is as rigorous as you implied here. https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_of_correctness https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o... > In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.
zahlman 1mo ago
I don't think this is a valid counterpoint at all. Math is cooperative, and comprehension is the point: the proof has value exactly because (and only to that extent) it empowers humans to understand an abstract truth. Chess is competitive: the memorized line has value because it makes you incrementally more likely to defeat your opponent.
- thechao 1mo ago
  I hope I'm remembering this right: a mathematician claims to have a proof for the ABC conjecture, but can't conceive any other mathematician it's right — it's "too weird", so the proof is rejected?
  - drdeca 1mo ago
    Not quite? It is more that 1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person 2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
  - sanxiyn 1mo ago
    The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything. https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
  - GPerson 1mo ago
    Some of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…
gowld 1mo ago
Math humans can use but not understand is called engineering. -- paraphrase of Bill Hammack, https://engineerguy.com https://engineerguy.com https://www.youtube.com/@engineerguyvideo https://www.youtube.com/@engineerguyvideo
fukaiall 1mo ago
Mate you managed to provoke with this comment. But you know what you’re saying right?

by kriro 1mo ago

GPerson 1mo ago

I don’t think it’s pointless to spend time trying to prove a conjecture which is ultimately false if along the way you figure out a bunch of different true variations on the conjecture, which is how mathematics actually works. This is something I’m a bit worried about with LLMs since it gets you to the end too fast.

ianm218 1mo ago
LLMs seem to have worse intuition than experts and compensate by being able to cover a much wider surface area of ideas, so we might just need to extract the intermediate progress along the way.

jhrmnn 1mo ago

I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?

metahuman_crumb 1mo ago
I suggest "Catching crumbs from the table" by Ted Chiang. Very short piece published in Nature (2000) and well worth a read. Depicts a scenario where modified humans produce science beyond ordinary scientists' comprehension.
- cfiggers 1mo ago
  This is a theme in Blindsight by Peter Watts as well. In that setting, field experts working at the bleeding edge are so advanced that non-experts literally can't understand what they're saying at all. So there's a whole class of specialists, "synthesists", that specialize in gaining approximate understanding of the experts' work for the purpose of communicating it to outsiders—perhaps wrongly, according to the expert at least, but hopefully more productively vs the unmediated version.
  - cfiggers 1mo ago
    What's amusing to me in this context is, summarizing emails and such has for a while been a supposed use case for AI—the LLM serving as the "synthesist" to explain long texts accessibly. But with this math question, a human "synthesist" would be needed to approximately understand the math discovered and programmatically verified by the LLM. So the roles reverse.
Jblx2 1mo ago
Mochizuki enters the chat
- OhNoNotAgain_99 1mo ago
  [dead]
JadeNB 1mo ago
Presumably there's not much logical obstruction to all human-understandable math eventually being formalized, although the willingness and ability to commit the requisite enormous amount of time will probably be insurmountable. But definitely that hasn't happened already!

RandomLensman 1mo ago

If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?

timjver 1mo ago
The whole point of Lean is that you don't need to understand the entire proof to be sure that it's correct. You only need to understand the definition of the theorem being proven, and you need to trust that the relatively small core of Lean is correct.
- RandomLensman 1mo ago
  Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
  - rowanG077 1mo ago
    Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
- gowld 1mo ago
  Why should you trust that the relatively small core of Lean is correct? The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.
- raincole 1mo ago
  I don't think Lean is as rigorous as you implied here. https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_of_correctness https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o... > In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.

zahlman 1mo ago

I don't think this is a valid counterpoint at all. Math is cooperative, and comprehension is the point: the proof has value exactly because (and only to that extent) it empowers humans to understand an abstract truth. Chess is competitive: the memorized line has value because it makes you incrementally more likely to defeat your opponent.

thechao 1mo ago
I hope I'm remembering this right: a mathematician claims to have a proof for the ABC conjecture, but can't conceive any other mathematician it's right — it's "too weird", so the proof is rejected?
- drdeca 1mo ago
  Not quite? It is more that 1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person 2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
- sanxiyn 1mo ago
  The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything. https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
- GPerson 1mo ago
  Some of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…

gowld 1mo ago

Math humans can use but not understand is called engineering. -- paraphrase of Bill Hammack, https://engineerguy.com https://engineerguy.com https://www.youtube.com/@engineerguyvideo https://www.youtube.com/@engineerguyvideo

fukaiall 1mo ago

Mate you managed to provoke with this comment. But you know what you’re saying right?