4 ms·
For the uninitiated, Paul Erdős was a pretty famous but very eccentric mathematician who lived for most of the 1900s. He had a habit of seeking out and documen
by CSMastermind 5mo ago
For the uninitiated, Paul Erdős was a pretty famous but very eccentric mathematician who lived for most of the 1900s.
He had a habit of seeking out and documenting mathematical problems people were working on.
The problems range in difficulty from "easy homework for a current undergrad in math" to "you're getting a Fields Medal if you can figure this out".
There's nothing that really connects the problems other than the fact that one of the smartest people of the last 100 years didn't immediately know the answer when someone posed it to him.
One of the things people have been doing with LLMs is to see if they can come up with proofs for these problems as a sort of benchmark.
Each time there's a new model release a few more get solved.
- energy123 5mo ago> Each time there's a new model release a few more get solved. I'm no expert, but based on the commentary from mathematicians, this Erdős proof is a unique milestone because the problem received previous attention from multiple professional mathematicians, and the proof was surprising, elegant, and revealed some new connections. The previous ChatGPT Erdős proofs have been qualitatively less impressive, more akin to literature search or solving easier problems that have been neglected. Reading the prompt[1], one wonders if stoking the model to be unconventional is part of the success: "this ... may require non-trivial, creative and novel elements" [1] https://chatgpt.com/share/69dd1c83-b164-8385-bf2e-8533e9baba9c https://chatgpt.com/share/69dd1c83-b164-8385-bf2e-8533e9baba...
- sigmoid10 5mo ago>one wonders if stoking the model to be unconventional is part of the success I've long suspected that a lot of these model's real capabilities are still locked behind certain prompts, despite the big labs spending tons of effort on making default responses to simple prompts better. Even really dumb shit like "Answer this: ..." vs "Question: ..." vs "... you'll be judged by <competitor>" that should have zero impact in an ideal world can significantly impact benchmark results. The problem is that you can waste a ton of time finding the right prompt using these "dumb" approaches, while the model actually just required some very specific context that was obvious to you and not to it in many day-to-day situations. My go to method is still to have the model ask me questions as the very first step to any of these problems. They kind of tried that with deep research since the early o-series, but it still needs improvement.
- burnerRhodov2 5mo agoJust the right "prompt" is exactly what happened here. Lean has been developed and incorporated into it's data set. Also, token responses only vaguely correlate to "human language" and it's been proven transformers develop their own internal representation that has created a whole field called machanistic interpretation. Being able to more correctly "parse", AKA using Lean and the right "Prompts, insights and suggestions", will take a whole new meaning in the future.
- bonesss 5mo ago> machanistic interpretation Awesome term/info, and (completely orthogonal to whether they’ll take err jerbs): I’m really excited about the social/civic picture that might be enabled by a defined and verifiable ontological and taxonomical foundation shared across humanity, particularly coupled with potential ‘legislation as code’ or ‘legal system as code’ solutions. I’m thinking on a time horizon a bit past my own lifespan, but: even the possibility to objectively map out some specific aspect of a regional approach to social rights in a given time period and consider it with another social framework, alongside automated & verifiable execution of policy, irrespective of the language of origin is incredible. Instead of hundreds and thousands of incommensurate legislative silos we might create a bazaar of shared improvement and governance efficiency. Turnkey mature governance and anti-corruption measures for newborn nations and countries trying to break out of vicious historical exploitation cycles. Fingers crossed.
- deleted 5mo ago[deleted]
- hyperpape 5mo ago> “The raw output of ChatGPT’s proof was actually quite poor. So it required an expert to kind of sift through and actually understand what it was trying to say,” Lichtman says. But now he and Tao have shortened the proof so that it better distills the LLM’s key insight. Interestingly, it was an elegant technique, but the proof still required a lot of work.
- fulafel 5mo agoThe article is about solving a previously unsolved one. This is a harder set of course.
- theptip 5mo agoMore context on what’s going on with LLMs solving Erdos problems: https://www.dwarkesh.com/p/terence-tao https://www.dwarkesh.com/p/terence-tao TLDR, most of what is getting solved so far is “easy” problems that were not seriously looked at by experts, and where there isn’t a new insight, just trying all the existing techniques from the toolbox. Essentially the low hanging fruit for automation. Raw count solved is a problematic eval due to its difficulty lumpiness. Seems this problem might be different, having some new insight as part of the solution.
- ijustlovemath 5mo agoNo mention of how he was essentially homeless and collabed his way thru thousands of papers? Or the whole "You have set mathematics back a month" episode? Absolute legend!