I find this whole post fascinating in the context of https://news.ycombinator.com/item?id=49738091 and particularly this excerpt from Gowers:

> Instead, I have a more complicated view, which I actually expressed in my essay The Two Cultures of Mathematics a quarter of a century ago, and which can be summarized by saying that there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding. At one end of the spectrum you have mathematicians who are primarily motivated by the wish to solve problems, who see conceptual understanding as a very important means to that end. At the other you have mathematicians who are primarily motivated by the wish to attain conceptual understanding, who see problem-solving as a very important means to that end.

Before, understanding and problem-solving-ability were so interdependent that distinguishing between the two was practically very difficult and probably wouldn’t have changed anyone’s research agenda. Now, they’re not connected, and this guy just did the ultimate meta-experiment of seriously undertaking a project that is intentionally 100% problem-solving and 0% understanding to prove it (maybe 99% and 1% but pretty close. In his transcripts, he never asks ChatGPT about the math, only about its opinions of the math).

As we (as a society) sit around asking ourselves what mathematicians (and software engineers, and anyone in deep technical fields) should be doing all day, we now have this case study to show us how wide our range of options has become.

▲

omnicognate 2 hours ago | parent | next [-]

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

▲

danabramov 2 hours ago | parent | next [-]

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

▲

dev_dan_2 21 minutes ago | parent | prev [-]

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

▲

31276ahq 2 hours ago | parent | prev [-]

Yes, the timing of this post just after Gowers' post is fascinating. It is almost as if the marketing machine is well oiled.

▲

danabramov 2 hours ago | parent | next [-]

What marketing machine? You think someone's paying me to do this?

▲

pfdietz an hour ago | parent | prev [-]

When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.

▲

3agha an hour ago | parent [-]

You can see by who entered the discussion (not you) and immediately sank certain comments that this is a protected submission. One wonders why.

	▲	pfdietz an hour ago \| parent [-]
		Or perhaps the criticisms are objectively unhinged and are so down voted without having to invent a conspiracy.