I’d be interested in understanding how Claude “helped” here, though AFAIK there are no details. I suspect it’s something like using the LLM to run some kind of optimised/filtered brute-force search and maybe getting a bit lucky, but maybe I’m way off base.
Matt Parker (stand up maths on YouTube) has a video from the last solved problem about how they did it.
This one? https://www.youtube.com/watch?v=ZJ8KThKAfbs
Edit: Huh, interesting. So there’s a few things going on:
- In some cases, LLMs have pulled together pre-existing knowledge that had not been connected before (sometimes across languages).
- Brute-forcing is sometimes part-of it (with searches informed by existing research)
- There are languages like LEAN that allow formal proofs to be written out and then tested logically. I guess this means that LLMs now have access to testing the logical validity of statements, which is helping to make a bunch of these most recent breakthroughs.
That last one is particularly interesting, I think, because it expands LLM capability from being language-focused (with interfaces for agentic work) to something that can actually understand (in a way) the validity of logical statements. I think it doesn’t get it to an understanding of truths in general, because logic is always built from axioms, and it can’t know the validity of the axioms (except by assumption). If I’m understanding things correctly)
The last one reminds me of months old paper named Darwin Gödel Machine, which uses similar approach to develop software by iteratively creating new ideas and improvements, from those implementations and then evaluations on tests. I think Google (or some other big corp) made something similar with different name and used it to improve matrix multiplication, which was published at the time as “AI improves itself”.
It is really nice approach and I love it, mainly because it resembles beautiful evolutionary algorithms.
Yeah… the AGI claims of LLM developers have run pretty hollow so far, but I can see how that could eventually lead in that direction. Wild.
I’m also way more interested in the details than the average news article on how AI can do maths now. Like how did they home in on this specific problem to solve? Destiny? Did they brute-force it and try 5000 other unsolved maths problems first? Was it AI assisted or does AI do this on its own? What’s the prompt? How many tokens did it burn through? Has it been lucky by chance or would I be able to input the same thing and there’s a 90% chance it’ll solve it again?
See the video linked in one of my other replies in this thread - a bunch of your questions are answered there (not for this specific case, but for a bunch of similar ones).
Wikipedia already has a full write up. It looks like Fable simply found an example of a function that had a constant Jacobian determinant (the determinant of the matrix of partial derivatives), but the function was not injective (3 different values of x, y, and z give the function the same value). Basically, the function is not “smooth”, so it can’t be inverted.
Thanks for adding that link. I had already read it before posting. Unfortunately it doesn’t include any meaningful details of how that function was found (presumably because the anthropic guy didn’t provide any yet).
Fortune magazine said he was unavailable for comment. To be honest, I wouldn’t answer Fortune magazine either.
Yeah… on the flip side, I also wouldn’t give any details if I was an anthropic employee hoping for an ambiguity-driven marketing boost.
I’m guessing that you’d…
1: Choose a math problem that’s difficult to solve, but easy to verify whether a solution is correct or not.
2: Set up a loop of two AIs talking to each other (or just two instances of one AI). The first is set up to come up with as many different solutions for the problem as possible, repeatedly, for many thousands of attempts. The second is tasked with checking each attempt to see whether it is actually a solution or not.
3: When the second AI flags something as a valid solution, have a human look over and check to see whether it really is or whether the second AI is just hallucinating. Hopefully, among just a few dozen false positives, you’ll find the actual valid solution.
Right, but I would think that would be a lot easier and more efficient to do via scripting than via an LLM. I guess you could get the LLM to write the scripts though…
I would say the mathematical proof could be extended or modified by infinitely many variants, so LLM could be used as a heuristic to guide the search based on similarities or previous approaches or just based on the context of the failing cases.
True, see my reply to another reply in this thread - it looks like that’s definitely happening in some cases.
edit: oh, you already replied to it 😅️