9 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 29d 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 29d 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 28d 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 29d 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 29d 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 29d 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 28d 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 29d ago
  Mochizuki enters the chat
  - OhNoNotAgain_99 29d ago
    [dead]
- JadeNB 28d 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 29d 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 29d 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 28d ago
    Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
    - rowanG077 28d 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 28d 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 28d 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 28d 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 28d 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?
  - ziiinq 28d ago
    [dead]
  - drdeca 28d 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 28d 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 28d ago
gowld 28d 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 28d ago
Mate you managed to provoke with this comment. But you know what you’re saying right?

by kriro 29d ago

GPerson 29d 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 28d 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 29d 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 29d 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 29d 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 28d 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 29d ago
Mochizuki enters the chat
- OhNoNotAgain_99 29d ago
  [dead]
JadeNB 28d 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 29d 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 29d 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 28d ago
  Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
  - rowanG077 28d 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 28d 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 28d 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 28d 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 28d 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?
- ziiinq 28d ago
  [dead]
- drdeca 28d 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 28d 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 28d ago

gowld 28d 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 28d ago

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