AI: Hard Fork in Mathematics  ## Document Notes ## Highlights - **AI Invents A Better Matrix Method** - Jaeden Schafer recounts Mo Goadet's keynote about AI discovering a new matrix multiplication method that boosted performance by 26%. - The change removed hundreds of millions in cost and energy for Google by inventing a new mathematical approach. Transcript: Jaeden Schafer He's a former Google X executive, and he was saying that AI is no longer just writing code. It's actually correcting human math. He gives this really incredible example where he says basically for the last 56 years, he's been using the same matrix multiplication method for code. And this is something that he said is like very standard. People agreed on this for a very long time. And he said that recently, he was, you know, talking to AI and telling it basically to improve itself. And he said when he told AI to improve itself, the AI realized that their matrix multiplication method was flawed. And so instead of trying to go and optimize the software that he had created that they had for AI, which is what he assumed it would do, instead, a completely new way of doing math. And he said to essentially optimize itself. And he said that that new invention resulted in a 26% in performance boost, and the removal of hundreds of millions of dollars in cost and energy use for Google. So like this massive uptick in basically optimization. ([Time 0:00:04](https://share.snipd.com/snip/bc925dc0-ab90-4a37-942a-5c7d3b90e1c7)) - **Models Solving Hard Math Quickly** - Jaeden Schafer highlights GPT-5 Pro solving Yudh Samarutsu's 554th problem in 15 minutes without internet searches. - This shows models are gaining strong elementary abstract algebra reasoning abilities. Transcript: Jaeden Schafer I wanted to start this off by saying that AI models right now are starting to crack a whole bunch of high level math problems. I was recently on X and I saw a tweet from Bartos Nasrekki where he said GPT-5 Pro solved in just 15 minutes without any internet searches the presentation problem known as Yudh Samarutsu's 554th problem. He said this is the first model to solve this task completely. He expects more of these kind of results. The model showed that it had a really strong grasp of elementary abstract algebra reasoning. So like these models are getting better and better at solving problems, but they're also doing really good in math competitions and other areas. Didi recently posted on X and said, AI just achieved a perfect score on the hardest math competition in the world. The Pootman has 12 problems and they each are worth 10 points the highest score last year was 90 the median was zero axioms ai pro prover in lear scored 120 out of 120 and just shared all Of the solutions huge milestone in ai i saw another really interesting story where over the weekend neil somani who is a software engineer he's a former quant, and now he has a startup. But he was testing how well OpenAI's newest AI model could handle really difficult math problems. ([Time 0:02:36](https://share.snipd.com/snip/307a3f47-f9f1-4c30-963f-75a9d470616d)) - **ChatGPT Solved An Unsolved Problem** - Jaeden Schafer tells Neil Somani's test where ChatGPT solved a long unsolved math problem in 15 minutes and verification tools confirmed it. - Somani examined the chain of reasoning and found the model's solution was actually correct. Transcript: Jaeden Schafer But he was testing how well OpenAI's newest AI model could handle really difficult math problems. And he said he had a he saw something that was really surprised him. Essentially, he pasted in a really long unsolved math problem. So there's these lists online, by the way, that like, there's one Hungarian mathematician. He's got like a thousand problems. He's posted online that have never been solved. And basically people take them and they put them into AI models to see if the AI model can solve them. And it's like, oh my gosh, like AGI is here. The AI model could solve it. Recently, we had one last year that Google's AI model solved. And so anyways, it's kind of always an exciting thing when they get solved. So he posted an unsolved math problem into ChatGPT. He let it run for 15 minutes. He came back and it had a solution for him, but you never know, right? Like maybe this is just hallucinated. So he goes and checks the solution and it turns out that it was actually right. There's kind of these online verification tools. One of them in particular is called Harmonic, and it's basically just designed to make sure that the logical arguments of solving a math problem are sound. And apparently once he pasted in ChatGPT's response, everything checked out. It said it was accurate. This is a quote from him. He said, I want to get a sense of where AI systems can actually solve open math problems and when they still get stuck. So I think he was really surprised by the fact that just how it had actually solved this problem. So problems that were previously out of reach, he says he thinks are now solvable. Okay, but I want to talk to you about how it solved this problem, its line of reasoning, because what's cool with ChatGPT and with reasoning is you can go and like look through its chain Of thought. And so he's obviously, he was a formulaic quant, he's a huge math nerd, so he can go and understand its chain of thought. And it was fascinating. ([Time 0:03:46](https://share.snipd.com/snip/2a5ab405-572c-4d2f-8bf0-e13be5ad8e43)) - **AI Synthesizes And Adapts Past Work** - Jaeden Schafer explains the model's method: research past results, connect ideas, and adapt older proofs to the new problem. - The model combined known theorems and an old MathOverflow post to craft a novel, more complete solution. Transcript: Jaeden Schafer Basically what it did is it pulled out a bunch of well-known ideas from mathematicians. So first it does research, it gets all of these, it tries to connect them in a logical way. In this particular case, it went and found some information about Legend's formula, Bertrand's prostulate, and the Star of David theorem. And then what absolutely blew my mind, it went and found an old math overflow post from 2013, where there was a Harvard mathematician named Noam Eliksiz, who had a really interesting Solution to a related problem, right? So not the same problem at all, but it was kind of a related problem. It goes and finds that. And then instead of copying just like the solution of how, you know, that former Harvard mathematician solved that problem, it took a completely different approach and ended up producing A much more complete answer to the question that was connected to some works of Paul Erdos, which is one of the most influential mathematicians of the 20th century. So I think for anyone that is skeptical about machine intelligence, this is amazing because this isn't just one isolated example. I think a lot of people are seeing like AI tools are already being used by a lot of different researchers. They're helping in a lot of different things, searching through academic papers and checking complex arguments. But I think since ChatGPT 5.2 came out, which is what Somani was using, he says that he has seen a huge shift in its reasoning, basically, than earlier versions. A lot of this is because of tooling. When you add, give tools to these models, different formulas and algorithms and calculators, like they're better. But its reasoning was so good. ([Time 0:05:32](https://share.snipd.com/snip/29d3bb69-0257-4e8c-9ea8-0e93a2a6e214)) - **AI Accelerates Solving Erdős Problems** - Jaeden Schafer notes 15 problems on the Erdős list moved from open to solved since Christmas. - Eleven of those published solutions explicitly mentioned using AI tools in the process. Transcript: Jaeden Schafer And I think since Christmas, 15 problems on the Eardose list have moved from open to solved. So open means, you know, like, here's the problem, no one has solved it, to have been officially solved. 11 of the cases, the published solution explicitly mentioned AI tools as part of the process. So whether, you know, that was like an AI model 100% solving the problem, or a human was most likely in a lot of these cases, a human was using AI tools to help them. 11 out of 15 of those iridus problems that got solved since Christmas were using AI tools. ([Time 0:07:56](https://share.snipd.com/snip/8c6a1070-c15d-4319-b5a1-d6608de0a2e2)) - **Tao: AI Is Helpful But Not Autonomous Yet** - Jaeden Schafer cites Terence Tao saying AI sometimes produces meaningfully new ideas and sometimes finds past research humans can build on. - Tao predicts fully independent AI mathematicians are far off but acknowledges current tools already matter a great deal. Transcript: Jaeden Schafer Terence Tao, he's one of the world's most respected mathematicians. He's basically tracked the progress carefully. And he says that in a whole bunch of different cases, AI systems produce meaningful, meaningfully new ideas on their own. But in other areas, they helped by finding relevant past research that humans could build on, right? Like in the case we were talking about earlier, you know, it was going in, it was finding some work that a Harvard mathematician had done, and it was kind of adapting it to its problem. But like, to be honest, that's still amazing, because it did come up with something new, and it did adapt it in a new way. So it's like, obviously, it's drawing on something. Anyways, I think, I think a lot of like, mathematicians say this, like, look, like, it's still using human research. Well, of course, it's using human research. Like, where do you think its training data came from? Where do you think it was, like, what was it fed? How can it do this? It's using human knowledge to be able to do this, but it is coming up with new novel things, which is interesting because, you know, at that rate, eventually it could just come up with Stuff without human knowledge, theoretically, right? That's kind of the interesting thing. ([Time 0:08:40](https://share.snipd.com/snip/15dfe2f5-f07a-47a7-a0e0-2cc24185880e)) - **Formal Verification Speeds Progress** - Jaeden Schafer explains translating natural-language proofs into verifiable formal formats makes checking easier and faster. - Coupling AI assistance with formal verification accelerates confirmation and reuse of mathematical results. Transcript: Jaeden Schafer So traditionally, proofs are written in natural language, which can hide a lot of the small mistakes or some of the unclear steps. So there's a bunch of new software tools that are allowing researchers to translate those arguments into a really precise format that can be automatically verified. This process is slow and it's tedious by hand, but if you're using an AI system, which of course these things are getting increasingly better at helping with, it makes it way easier to Confirm results and then also to build on them, because the faster you can actually check that the AI model or even a person solved a problem correctly, the faster you can say, okay, here's How we solve this type of problem. Now we'll use this kind of as a building block for future problems in this direction, and there's more problems that you can solve. ([Time 0:10:38](https://share.snipd.com/snip/6eeae695-b5a3-4a94-90fd-4f52c2fd32f5)) - **Get Trusted Researchers To Use Tools** - Jaeden Schafer shares Tudor Archimick's point: adoption by careful professors is the key signal of tool credibility. - Encourage respected researchers to use AI verification tools to build trust and accelerate adoption. Transcript: Jaeden Schafer It's this tool that checks the math problems, and his name's Tudor Archimick. And something that he said that's really interesting is that the most important signal is not how many problems actually get solved, but who's willing to use the tools. Here's a quote from him. He said, what matters is that serious math and computer science professors are actually using them. These are people whose careers depend on being careful and credible. So when they say they rely on AI tools, that says a lot. And honestly, I think it really does. ([Time 0:11:21](https://share.snipd.com/snip/119b7ef0-4ad8-4246-9727-6b654eaf1c56)) - **Math Advances Multiply Across Fields** - Jaeden Schafer argues AI mathematical reasoning will boost many fields like engineering, economics, and medicine. - Improved AI reasoning and verification can dramatically speed research and innovation beyond mathematics. Transcript: Jaeden Schafer Because the same abilities that help an AI reason through on, you know, for example, like an abstract problem, it could still, it can actually be used and applied into fields like engineering, Economics, medicine, science, right? Like progress in a lot of those fields is often slow because problems are really complex. They're hard to verify. So as the AI systems get better at actually exploring ideas and checking work and connecting past knowledge, they are going to dramatically speed up research and innovation. So for me, the advancements being made in AI and math isn't just exciting for math, but for so many other areas that are going to benefit and the reasoning capability of these models improving Means that so many different areas are going to improve, including software engineering, which personally is getting me really excited this week. ([Time 0:11:51](https://share.snipd.com/snip/4b20ee76-7d89-42f9-89df-d91f090936c9))