alt Hacker NewsTerence Tao says something surprisingly similar in a recent talk (https://news.ycombinator.com/item?id=49056620 ) Not that the proof is worthless but that the value comes after it's revised into a cleanly understandable form and then canonicalized so that other mathematicians can use it.
Replies
vessenes • yesterday at 9:44 PM
I'd like to note that we should remember a formalized Lean proof does have value in that it enters the pantheon of true things other Lean proofs can rely on. Agreed that for the humans, descriptions and being able to 'grok' the proof / assess it for new tools and concepts is extremely helpful.
dr_scully • yesterday at 8:32 PM
He also made a video on the same topic for Big Think: https://news.ycombinator.com/item?id=49551848
Tao is saying that there is very little insight from something like an LLM counterexample (e.g. Jacobian conjecture counterexample he investigated further on his blog) - you don't learn much about the subject and _why_ a conjecture was true or false from an LLM giving a counterexample. That's why he wrote the blog post - to analyse what the counterexample says about the subject.
Tao does not disbelieve the counterexample (it's seemingly easy enough for him to verify it is a counterexample).
Parent is saying something very different - they're saying they literally don't have any faith that this is a proof. Given its size, it could just be a bunch of completely useless statements that do pass the type checker.