> I genuinely invite a refutation.

> So, assuming my proof doesn’t rely on a Lean kernel bug, it’s likely to be legit too.

He lacks the understanding to verify his solution properly, and has to lean on those who do have the understanding to verify it, only being able to say himself that it's "likely" to be correct. (And what do those mathematicians get for laboriously checking the generated proof? 40 grand?)

Seems to me problem solving is as dependent on understanding as ever.

▲

danabramov 2 hours ago | parent [-]

Author here. No one's asking mathematicians to check the generated proof. I explain it in this part: https://overreacted.io/how-i-vibed-a-proof-of-conways-conjec...

The only thing that needs a check is this 500-line file: https://github.com/gaearon/conway-refinement/blob/264445c93b.... If this file is correct and Lean kernel is correct, the proof is correct.

Moverover, the version I linked above is intentionally paranoid so it doesn't use any third-party code except Mathlib. If you allow usage of CombinatorialGames and trust its definitions, the part that needs to be checked narrows down to exactly 20 lines of code: https://github.com/gaearon/conway-refinement/blob/264445c93b...

▲

an hour ago | parent | next [-]

[deleted]

▲

omnicognate 2 hours ago | parent | prev [-]

> If this file is correct and Lean kernel is correct, the proof is correct

There are two ifs in this sentence.

▲

dev_dan_2 19 minutes ago | parent | next [-]

What is your point? Please don't be obtuse, it is more constructive to make your points clearly.

▲

danabramov 2 hours ago | parent | prev [-]

What is your point, exactly? Increasing number of people working in and around mathematics are relying on Lean kernel's correctness. That's kind of the point of tools like Lean. Why is it a problem for me to publish a result that relies on it? How do you think other Lean proofs work?

▲

omnicognate an hour ago | parent [-]

My point is what I said. Without understanding you are only able to say your proof is "likely" to be correct. It's clear from your writing that you understand that your proof will only be accepted once thoroughly reviewed by human mathematicians, who will certainly not be just verifying the definition. Bugs in Lean exist (you're a programmer and it's a program, why would you assume they don't?) and reward hacking and finding bugs are both well established LLM behaviours.

> 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".

	▲	danabramov 11 minutes ago \| parent [-]
		I see, we don't seem to disagree much. 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 checking 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.