undefined

points

[-]

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.

by well_ackshually5 hours ago|

parent|

[-]

You're putting a lot of words in my mouth. What I'm saying is that whether or not it's a proof, it's useless: it does not improve human knowledge, because the only thing able to consume 10MB of Lean to build upon it is another LLM that's going to build a 50MB piece of shit.

It's very much likely a proof. It's also completely useless.

by asib4 hours ago|

parent|

[-]

You said:

> For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean.

So you were implying the possibility of there not actually being a proof at all.

Anyway, I disagree. I'd refer you to Tao's blog post about the Jacobian conjecture counterexample.

The existence of a proof is something you can use, with an LLM, to derive insight, just as Tao did with the existence of the counterexample.

by dr_scully8 hours ago|

prev|

[-]

He also made a video on the same topic for Big Think: https://news.ycombinator.com/item?id=49551848

by vessenes7 hours ago|

prev|

[-]

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.