alt Hacker NewsThe 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.
Replies
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.
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?
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?
Mate you managed to provoke with this comment. But you know what you’re saying right?
Math humans can use but not understand is called engineering. -- paraphrase of Bill Hammack, https://engineerguy.com
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.