I find this whole post fascinating in the context of <a href="https://news.ycombinator.com/item?id=49738091">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.
> 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.
Author here. No one's asking mathematicians to check the generated proof. I explain it in this part: <a href="https://overreacted.io/how-i-vibed-a-proof-of-conways-conjecture/#hardening-the-audits" rel="nofollow">https://overreacted.io/how-i-vibed-a-proof-of-conways-conjec...
The only thing that needs a check is this 500-line file: <a href="https://github.com/gaearon/conway-refinement/blob/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/Mathlib/InlineConwayRefinement.lean" rel="nofollow">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: <a href="https://github.com/gaearon/conway-refinement/blob/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/CombinatorialGames/ConwayRefinement.lean#L27-L46" rel="nofollow">https://github.com/gaearon/conway-refinement/blob/264445c93b...
msteffen · · focus · HN ↗
> 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 · · focus · HN ↗
> 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 · · focus · HN ↗
The only thing that needs a check is this 500-line file: <a href="https://github.com/gaearon/conway-refinement/blob/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/Mathlib/InlineConwayRefinement.lean" rel="nofollow">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: <a href="https://github.com/gaearon/conway-refinement/blob/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/CombinatorialGames/ConwayRefinement.lean#L27-L46" rel="nofollow">https://github.com/gaearon/conway-refinement/blob/264445c93b...
[deleted] · · focus · HN ↗
[deleted]