> If this file is correct and Lean kernel is correct, the proof is correct
There are two ifs in this sentence.
There are two ifs in this sentence.
> Why is it a problem for me to publish a result that relies on it?
Bit over-sensitive here. I never said it was a problem for you to publish a result. You can do what you like on your blog and spend your tokens however you choose, just as I'm free to have my own opinions on the value of such an effort. I was responding to, and disputing, a commenter's assertion that understanding and problem-solving ability are "now ... not connected".
While Lean is tightening things up after the recent LLM-driven hacks, I agree that bugs are possible. Although usually code that exploits them is obviously aggressive and is deliberately using the more obscure features related to metaprogramming. Also note that my solution has passed the nanoda kernel as well (https://palomar-registry.org/entry?id=PALOMAR-2026-09-03-000...).
That said, again, I never implied that I'm asking mathematicians to "laboriously [check] the generated proof" which is what your parent comment says. The value to mathematicians is knowing that the conjecture is probably right, and knowing the rough path the LLM has taken to it. Instead of checking the Lean proof line by line, what mathematicians are interested in doing (at least, the ones I've been in contact with) is finding a shorter and more direct proof now that they're aware of the outline and main intermediate claims. As for how much value they find in that, I presume they would be able to speak to that when/if they would like to make their research public.
Ah, or is the value to mathematicians that their LLMs can build results on top of this? (In which case, did this do more than save them some tokens?) Or is the value the deep mathematical insight that this result incidentally gives a few mathematicians the confidence to develop for their own personal satisfaction (e.g. if they decide to go and prove it for themselves, and come to the same result after a lot of work)?
(IMO, the deep, scary question: what if it’s soon impossible to make anything at all that anyone who doesn’t know you personally would bother to look at or use? https://www.smbc-comics.com/comic/crack)