3 ms·

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

I find this whole post fascinating in the context of 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.

31276ahq 16d ago
Yes, the timing of this post just after Gowers' post is fascinating. It is almost as if the marketing machine is well oiled.
- danabramov 16d ago
  What marketing machine? You think someone's paying me to do this?
- pfdietz 16d ago
  When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.
  - 3agha 16d ago
    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 16d ago
      Or perhaps the criticisms are objectively unhinged and are so down voted without having to invent a conspiracy.
omnicognate 16d ago
> 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 16d ago
  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-conjecture/#hardening-the-audits 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/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/Mathlib/InlineConwayRefinement.lean 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/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/CombinatorialGames/ConwayRefinement.lean#L27-L46 https://github.com/gaearon/conway-refinement/blob/264445c93b...
  - omnicognate 16d ago
    > If this file is correct and Lean kernel is correct, the proof is correct There are two ifs in this sentence.
    - danabramov 16d ago
      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?
simianwords 15d ago
Perhaps mathematicians will undergo the same split as what happened to philosophy and natural sciences.

31276ahq 16d ago

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

danabramov 16d ago
What marketing machine? You think someone's paying me to do this?
pfdietz 16d ago
When you descend into conspiracy theorizing to defend your prejudices, it's time to stop and reconsider.
- 3agha 16d ago
  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 16d ago
    Or perhaps the criticisms are objectively unhinged and are so down voted without having to invent a conspiracy.

omnicognate 16d ago

> 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 16d ago
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-conjecture/#hardening-the-audits 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/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/Mathlib/InlineConwayRefinement.lean 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/264445c93b78554c408e99e4e7f663693b4e91ab/ConwayRefinement/Standalone/CombinatorialGames/ConwayRefinement.lean#L27-L46 https://github.com/gaearon/conway-refinement/blob/264445c93b...
- omnicognate 16d ago
  > If this file is correct and Lean kernel is correct, the proof is correct There are two ifs in this sentence.
  - danabramov 16d ago
    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?

simianwords 15d ago

Perhaps mathematicians will undergo the same split as what happened to philosophy and natural sciences.