Comment by newmana

Comment by newmana 2 days ago

9 replies

"Recently, yet another category of low-hanging fruit has been identified as within reach of automated tools: problems which, due to a technical flaw in their description, are unexpectedly easy to resolve. Specifically, problem #124 https://www.erdosproblems.com/124 was a problem that was stated in three separate papers of Erdos, but in two of them he omitted a key hypothesis which made the problem a consequence of a known result (Brown's criterion). However, this fact was not noticed until Boris Alexeev applied the Aristotle tool to this problem, which autonomously located (and formalized in Lean) a solution to this weaker version of the problem within hours."

https://mathstodon.xyz/@tao/115639984077620023

adastra22 2 days ago

That doesn’t seem very fair. The problem was stated, and remained unsolved for all this time. You can’t take away that accomplishment just because the solution seems easy in hindsight.

  • zozbot234 2 days ago

    It's technically true that this version of the problem was "low-hanging fruit", so that's an entirely fair assessment. Systematically spotting low-hanging fruit that others had missed is an accomplishment, but it's quite different from solving a genuinely hard problem and we shouldn't conflate the two.

    • adastra22 2 days ago

      My point is stronger than that. Some things only appear low hanging fruit in hindsight. My own field of physics is full of examples. Saying “oh that should’ve been easy” is wrong more often than it is right.

      • ak_111 2 days ago

        It’s a combination of the problem appearing to be low-hanging fruit in hindsight and the fact that almost nobody actually seemed to have checked whether it was low-hanging in the first place. We know it’s the latter because the problem was essentially uncited for the last three decades, and it didn't seem to have spread by word of mouth (spreading by word of mouth is how many interesting problems get spread in math).

        This is different from the situation you are talking about, where a problem genuinely appears difficult, attracts sustained attention, and is cited repeatedly as many people attempt partial results or variations. Then eventually someone discovers a surprisingly simple solution to the original problem which basically make all the previous paper look ridiculous in hindsight.

        In those cases, the problem only looks “easy” in hindsight, and the solution is rightly celebrated because there is clear evidence that many competent mathematicians tried and failed before.

        Are there any evidence that this problem was ever attempted by a serious mathematician?

      • zozbot234 2 days ago

        Sure, but unless all solvable problems can be said to "appear as low-hanging fruit in hindsight" this doesn't detract from Tao's assessment in any way. Solving a genuinely complex problem is a different matter than spotting simpler solutions that others had missed.

        In this case, the solution might have been missed before simply because the difference between the "easy" and "hard" formulations of the problem wasn't quite clear, including perhaps to Erdős, prior to it being restated (manually) as a Lean goal to be solved. So this is a success story for formalization as much as AI.