OpenAI, Anthropic Models Crack Historic Math Problems via Lean Proofs

The summer Math fell to the machines... — Fireship

Fireship

Automated frontier AI systems pairing multi-agent swarms with compiler-verified Lean certificates have resolved more open mathematical conjectures in three weeks than human researchers solved over the prior decade, bypassing traditional peer review.

AI-assisted summary of The summer Math fell to the machines... — original source. Check the original for full context.

Source published:

Key ideas

  • Over a span of just three weeks, AI models eliminated more open mathematical problems than human mathematicians managed to solve in the entire preceding decade. (0:00)
  • Levent Alpoge used an AI tool called Fabel to disprove the 87-year-old Jacobian conjecture, one of Stephen Smale's famous problems for the 21st century. (1:12)
  • OpenAI and Anthropic paired major breakthroughs with machine-checked Lean proof certificates, moving verification away from traditional human peer review. (2:24)
  • Anthropic's Claude Code deployed a 60-agent swarm that shifted the proven fraction of non-trivial zeros on the Riemann hypothesis critical line from 41% to 67%. (4:00)

Detailed notes

## Background Published by the tech and programming YouTube channel Fireship on August 19, 2026, this video covers a sudden wave of automated mathematical breakthroughs. The video description highlights that artificial intelligence eliminated more long-standing open math problems in a span of weeks than human mathematicians managed to solve over the previous decade.

## TL;DR While software engineers long feared being replaced by artificial intelligence, professional mathematicians experienced a sudden disruption as frontier AI models dismantled decades-old open problems in rapid succession. AI systems brought down iconic benchmarks, including an 80-year-old Erdős conjecture, the 87-year-old Jacobian conjecture, and graph routing problems shattered with minimal prompting. Major research labs scaled the trend with formal machine-checked Lean proofs, culminating in an unreleased Anthropic agent swarm directed by Bun creator Jared Sumner that raised the unconditional bound on the Riemann hypothesis from 41% to 67%.

## Atmosphere & style Delivered in Fireship's signature rapid-fire, sardonic cadence, the video blends dark tech humor with genuine disbelief at the speed of machine-driven mathematical progress. The narrative arc moves briskly from mocking software engineers' existential dread to cataloging the real panic spreading through elite academia, complete with witty pop-culture quips about child prodigies and rich tech founders on jogs. It feels dizzying and kinetic, capturing the eerie sensation of watch-checking as decades of human mathematical theory fall to simple prompts and agent swarms in real time.

## Bulletin - [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) Over a span of just three weeks, AI models eliminated more open mathematical problems than human mathematicians managed to solve in the entire preceding decade. - [01:12](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=72s) Levent Alpoge used an AI tool called Fabel to disprove the 87-year-old Jacobian conjecture, one of Stephen Smale's famous problems for the 21st century. - [02:24](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=144s) OpenAI and Anthropic paired major breakthroughs with machine-checked Lean proof certificates, moving verification away from traditional human peer review. - [04:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=240s) Anthropic's Claude Code deployed a 60-agent swarm that shifted the proven fraction of non-trivial zeros on the Riemann hypothesis critical line from 41% to 67%.

## Key takeaways - [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) While software developers largely weathered early fears of AI obsolescence, mathematicians faced an abrupt wave of machine-driven disruption. - [00:31](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=31s) Terence Tao warned at the International Congress of Mathematicians that AI breakthroughs represent an impending crisis for foundational research practices. - [00:47](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=47s) Academic interest pivoted from competitive IMO problem-solving to real concern after an OpenAI model disproved an 80-year-old Erdős unit distance conjecture. - [01:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=60s) The Leiden Declaration, drafted by 16 researchers across 15 universities calling for formal guardrails on AI mathematics research, was largely ignored. - [01:12](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=72s) The 1939 Jacobian conjecture in algebraic geometry fell when mathematician Levent Alpoge formulated a counterexample assisted by the AI tool Fabel. - [02:24](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=144s) Dimitri Rybin broke the 30-year-old Garg-Könemann graph routing conjecture using GPT-5.6 with four prompts totaling just 58 words. - [02:40](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=160s) The Garg-Könemann counterexample proved shipping costs can unavoidably increase when bundling split paths using a graph of seven nodes and nine edges. - [03:04](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=184s) Automated mathematics research democratized rapidly, with graduate students and independent amateurs solving multiple open Erdős problems in single weeks. - [03:16](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=196s) OpenAI resolved ten open problems simultaneously, releasing corresponding code repositories validated by compiler-checked Lean certificates. - [03:38](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=218s) Key institutional AI wins included raising the 1978 sphere-packing bound, constructing a non-Desarguesian group, and refuting Connes' rigidity conjecture. - [04:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=240s) Prompted casually by Bun creator Jared Sumner, Anthropic's Claude Code mobilized 60 sub-agents, 2,400 shell commands, and 31 million tokens over 36 hours. - [04:45](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=285s) Claude Code's Riemann hypothesis effort advanced the unconditional proportion of zeros on the critical line from 41% to 67%, verified by external number theorists and Lean.

## Detailed walkthrough ### [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) The Math Apocalypse Begins: Erdős, the Jacobian, and Quick AI Kills

For years, software developers have endured relentless warnings that artificial intelligence would render them obsolete and "steal the food they've been putting on their family." Yet aside from the occasional existential dread, most programmers are doing just fine. The same cannot be said for mathematicians. Over a span of just three weeks, AI models eliminated more open mathematical problems than human mathematicians managed to solve across the entire previous decade. The disruption arrived at breakneck speed: an 87-year-old conjecture pulled straight from the list of the hardest mathematical problems of the 21st century was disproven during the World Cup final, while a 30-year-old graph theory conjecture crumbled under a mere four prompts totaling 58 words.

The shockwaves reached the highest echelons of the field. Terence Tao—a prodigy who earned an International Mathematical Olympiad medal at age 10 while ordinary children were busy "making cinnamon sugar sandwiches and watching *Rocket Power*"—took the stage at the International Congress of Mathematicians to issue a stark warning about a looming crisis in the core values and foundational practices of mathematics. The shift traces back roughly a year prior, when AI systems managed to solve five out of six problems at the IMO. At the time, the achievement felt relatively harmless to working academics, who dismissed competition mathematics as little more than the "LeetCode of math problems." However, the tone shifted dramatically in May when an OpenAI model disproved an 80-year-old Erdős conjecture concerning unit distances, leaving researchers sleepless and rattled. In June, 16 researchers across 15 universities attempted to intervene by publishing the Leiden Declaration, an appeal urging the scientific community to establish formal guardrails around AI-driven mathematics research—a request the broader world promptly ignored.

Matters escalated further in July. While spectators were glued to summer sports and European heatwaves, mathematician Levent Alpoge published a counterexample on X that decisively disproved the Jacobian conjecture, an iconic open problem in algebraic geometry dating back to 1939. The conjecture states that if a polynomial function has an invertible derivative everywhere—meaning it is locally reversible no matter how close you zoom in—the function as a whole must also be globally reversible. Because this property felt intuitively true to generations of mathematicians, it earned a spot on Stephen Smale's famous list of major problems for the 21st century. Alpoge brought the 87-year-old problem down using assistance from an AI tool called Fabel.

- **May Erdős Disproof:** An OpenAI model shattered an 80-year-old Erdős conjecture on unit distances, sparking immediate insomnia among senior researchers. - **The Leiden Declaration:** Drafted by 16 researchers from 15 universities to demand AI research guardrails, which were completely bypassed by the community. - **Smale's Problem Struck Down:** The Jacobian conjecture, unresolved since 1939, fell after Levent Alpoge constructed a counterexample with AI assistance.

[02:24](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=144s) Cheap Prompts and Mass Casualties: From Graph Theory to Sphere Packing

Just two days after the Jacobian conjecture fell, another long-standing problem succumbed to minimal effort. The 30-year-old dense Garg-Könemann conjecture in graph theory concerns network routing: if shipments are permitted to split across multiple pathways, can they always be bundled into single, unsplit paths without driving up overall delivery costs? For three decades, the mathematical community assumed this property held true without ever managing to prove it. Researcher Dimitri Rybin tested the hypothesis by pointing GPT-5.6 at it, effectively prompting the model to make a breakthrough. The model swiftly responded with a tiny counterexample—a graph consisting of just seven nodes and nine edges—demonstrating that forcing shipments into a single path was unavoidably more expensive than splitting them, thereby shattering the conjecture in minutes.

The democratization of these automated breakthroughs quickly spread beyond elite research institutes. Over the course of the same week, a Columbia University PhD student knocked down six open Erdős problems in five days, while an independent 23-year-old amateur solved another. Soon after, major AI laboratories entered the fray with institutional scale. OpenAI announced that an internal version of its next frontier model had solved ten open problems spanning mathematics and theoretical computer science. Crucially, they verified every result by committing code repositories to GitHub paired with Lean certificates—machine-checked proofs verified mechanically by a compiler rather than human peer review.

```mermaid flowchart TD accTitle: AI Mathematical Problem Solving Pipeline accDescr: Progression from human prompting to automated problem-solving and machine verification in Lean.

subgraph Input["Input & Execution"] P["Natural Language Prompts"] --> LLM["Frontier AI Models<br/>(GPT-5.6 / Claude Code)"] LLM --> S["Automated Agent Workflows<br/>(Scripts & Multi-Agent Swarms)"] end

subgraph Discoveries["Mathematical Discoveries"] S --> C1["Graph Routing Counterexample<br/>(7 nodes, 9 edges)"] S --> C2["Sphere Packing Bounds<br/>(Improved 1978 baseline)"] S --> C3["Riemann Hypothesis Solutions<br/>(Shifted to 67% probability)"] end

subgraph Verification["Validation"] C1 --> L["Lean Proof Certificates"] C2 --> L C3 --> L L --> V["Deterministic Compiler Verification"] end ```

OpenAI's haul included an improvement to the general upper bound on sphere packing—the classic question of how densely identical spheres can be crammed into high-dimensional space—a threshold that had remained entirely unmoved since 1978. Their model also produced the first explicit construction of a non-Desarguesian group and disproved Alain Connes' rigidity conjecture, resolving questions mathematicians had actively chased since the 1990s.

- **Trivial Prompts, Big Breakthroughs:** Dimitri Rybin broke a 30-year routing conjecture with just four prompts and 58 words, exposing a 7-node, 9-edge counterexample. - **Grassroots Proving Spree:** Six open Erdős conjectures solved in five days by a single Columbia graduate student, followed by another solved by an amateur. - **Formal Verification Standards:** OpenAI published ten simultaneous solutions to open problems accompanied by machine-verifiable Lean proof certificates. - **Key Open Problems Toppled:** Breakthroughs included raising the 1978 sphere-packing bound, constructing a non-Desarguesian group, and refuting Connes' rigidity conjecture.

[04:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=240s) Jared Sumner's Jog and the Riemann Hypothesis

Competition between the leading frontier labs soon spilled over into the most prestigious unsolved problem in mathematics: the Riemann hypothesis. Unwilling to let OpenAI capture all the glory, Anthropic revealed that an unreleased model had made substantial headway on the 167-year-old Millennium Prize Problem governing the distribution of prime numbers—an achievement bearing an official million-dollar prize bounty.

The catalyst for this breakthrough was not a staff mathematician, but Jared Sumner, the creator of Bun, who decided to prompt the model while out on a run during his "filthy rich now and need to get fit, too, era." Sumner casually asked Claude to make a serious attempt at proving the Riemann hypothesis. The AI initially hallucinated 650 incorrect ideas. When Sumner instructed it to try again, Claude Code orchestrated a massive internal swarm:

> "This time the model spent a day and a half coordinating 60 sub-agents inside Claude Code, running 2,400 shell commands, writing hundreds of Python scripts, and burning 31 million output tokens."

While the agent swarm did not produce a full, definitive proof of the Riemann hypothesis, it succeeded in shifting the established fraction of non-trivial zeros that unconditionally lie on the critical line from 41% to 67%. The mathematical leap was subsequently audited and confirmed by two Anthropic in-house mathematicians, evaluated by two independent external number theorists, and formally encoded as a certified proof in Lean. The presentation concludes with a brief shoutout to sponsor Railway, praised for offering zero-friction deployments without subjecting viewers to an overly long advertisement.

- **Riemann Progress Metrics:** Advanced the confirmed proportion of solutions satisfying the Riemann hypothesis from 41% up to 67%. - **Compute Footprint:** Required 36 hours of continuous coordination, 60 sub-agents, 2,400 shell executions, hundreds of Python scripts, and 31 million tokens. - **Independent Validation:** Verified by two internal Anthropic specialists, two external number theorists, and compiled into Lean.

## Notable quotes > [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) steal the food they've been putting on their family

> [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) making cinnamon sugar sandwiches and watching Rocket Power

> [00:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=0s) LeetCode of math problems

> [04:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=240s) This time the model spent a day and a half coordinating 60 sub-agents inside Claude Code, running 2,400 shell commands, writing hundreds of Python scripts, and burning 31 million output tokens.

> [04:00](https://www.youtube.com/watch?v=iuZPTE5qsJY&t=240s) filthy rich now and need to get fit, too, era

## Mentioned Fireship, Railway, Terence Tao, International Mathematical Olympiad (IMO), International Congress of Mathematicians, OpenAI, Paul Erdős, Leiden Declaration, Levent Alpoge, Jacobian conjecture, Stephen Smale, Fabel, dense Garg-Könemann conjecture, Dimitri Rybin, GPT-5.6, Columbia University, Lean, GitHub, Alain Connes, Anthropic, Riemann hypothesis, Jared Sumner, Bun, Claude, Claude Code, Python

## Video description Railway is the smoothest way to deploy software. Get $20 in free credits - https://railway.com/?referralCode=fireship

AI has killed more open math problems in the last few weeks than the entire human race managed in the previous decade. Let's dive in.

#coding #programming

Want more Fireship?

🗞️ Newsletter: https://bytes.dev 🧠 Courses: https://fireship.dev

[Source](https://www.youtube.com/watch?v=iuZPTE5qsJY)

中文简报

OpenAI与Anthropic模型借助Lean证明攻克历史性数学难题 前沿自动化AI系统将多智能体集群与经编译器验证的Lean凭证相结合，在三周内解决的未决数学猜想数量超过了人类研究人员在过去十年解决的总和，绕过了传统同行评审。 尽管软件工程师长期以来一直担忧被人工智能取代，但随着前沿AI模型接连破解困扰学界数十年的开放性难题，专业数学家正经历突如其来的颠覆。AI系统攻克了多个标志性难题，包括拥有80年历史的Erdős猜想、87年历史的雅可比猜想（Jacobian conjecture），以及仅凭极少提示词便化解的图路由问题。各大主流研究实验室利用机器验证的形式化Lean证明拓展了这一趋势，最终在Bun创造者Jared Sumner指导的一套未发布的Anthropic智能体集群推动下，将黎曼猜想的无条件界限从41%提升至67%。 在短短三周时间内，AI模型攻克的未决数学问题数量超过了人类数学家在过去整整十年中解决的总和。 (0:00) Levent Alpoge利用名为Fabel的AI工具证伪了拥有87年历史的雅可比猜想，该猜想是Stephen Smale提出的著名21世纪数学难题之一。 (1:12) OpenAI和Anthropic将重大突破与机器验证的Lean证明凭证相结合，使结果验证脱离了传统的同行评审模式。 (2:24) Anthropic的Claude Code部署了一个由60个智能体组成的集群，将黎曼猜想临界线上已证明的非平凡零点比例从41%提升至67%。 (4:00)

Reading summary

According to a report by Fireship, while software developers have largely withstood predictions of AI obsolescence, theoretical mathematics experienced a sudden upheaval when AI models solved more open problems in three weeks than human mathematicians had across the previous decade. This rapid automation has overturned decades-old conjectures, democratized proof discovery, and prompted warnings about the foundational practices of the discipline. Academic Alarm and the Fall of Major Conjectures (0:00) Working academics initially dismissed AI systems solving five of six International Mathematical Olympiad problems a year prior as the "LeetCode of math problems." That complacency ended in May when an OpenAI model disproved an 80-year-old Erdős conjecture on unit distances. In July, mathematician Levent Alpoge used an AI tool called Fabel to produce a counterexample disproving the 1939 Jacobian conjecture. Because the conjecture—which posits that a locally reversible polynomial function must be globally reversible—felt intuitively true, it had been included on Stephen Smale's list of major 21st-century problems. These developments rattled researchers and reached the highest levels of the field. At the International Congress of Mathematicians, prodigy Terence Tao warned of a looming crisis in the core values and foundational practices of mathematics. Earlier in June, 16 researchers across 15 universities published the Leiden Declaration to demand formal guardrails around AI-driven mathematics research, though the broader community ignored the appeal. Low-Effort Prompts and Democratized Discovery (2:24) Beyond high-profile problems, AI models have drastically lowered the barrier to refuting established assumptions. Researcher Dimitri Rybin used just four prompts totaling 58 words with GPT-5.6 to test the 30-year-old dense Garg-Könemann conjecture in graph theory, which assumed network shipments could be bundled into single paths without increasing delivery costs. Within minutes, the model returned a counterexample consisting of seven nodes and nine edges, proving that single-path routing is unavoidably more expensive. This accessibility has enabled rapid breakthroughs outside elite research institutions. Within a single week, a Columbia University PhD student solved six open Erdős problems in five days, and an independent 23-year-old amateur resolved another. Frontier Lab Scale and Machine Verification (4:00) Major AI laboratories have paired frontier models with automated verification to solve problems at institutional scale. OpenAI announced that an internal frontier model solved ten open problems across mathematics and theoretical computer science. These included improving the 1978 general upper bound on high-dimensional sphere packing, constructing the first explicit non-Desarguesian group, and disproving Alain Connes' rigidity conjecture from the 1990s. Rather than relying solely on human peer review, OpenAI committed code repositories to GitHub with Lean certificates—machine-checked proofs verified by a compiler. In response, Anthropic revealed progress on the 167-year-old Riemann hypothesis, a Millennium Prize Problem with a million-dollar bounty governing prime number distribution. Prompted by Bun creator Jared Sumner while on a run, an unreleased model initially hallucinated 650 incorrect ideas. When told to try again, Claude Code spent 36 hours coordinating 60 sub-agents, running 2,400 shell commands, writing hundreds of Python scripts, and consuming 31 million output tokens. While it did not achieve a complete proof, it increased the confirmed fraction of non-trivial zeros on the critical line from 41% to 67%, a result audited by two internal Anthropic mathematicians, two external number theorists, and compiled into Lean. While AI agent swarms and frontier models have not yet completely solved foundational challenges like the Riemann hypothesis, their ability to generate compiler-verified proofs and counterexamples in hours or days has bypassed academic calls for guardrails and altered how open mathematical problems are resolved.

Source quotes

[0:00] steal the food they've been putting on their family [0:00] making cinnamon sugar sandwiches and watching Rocket Power [0:00] LeetCode of math problems [4:00] This time the model spent a day and a half coordinating 60 sub-agents inside Claude Code, running 2,400 shell commands, writing hundreds of Python scripts, and burning 31 million output tokens. [4:00] filthy rich now and need to get fit, too, era

Original transcript

[0:00] For years now, every developer has had [0:01] to put up with hearing about how AI is [0:03] going to make them obsolete and steal [0:05] the food they've been putting on their [0:06] family. But, besides the occasional [0:08] identity crisis, I feel like most of us [0:10] are actually doing pretty well. Sadly, [0:13] our mathematician friends may not be so [0:15] lucky because over the last 3 weeks, AI [0:17] has killed more open math problems than [0:19] the entire human race managed in the [0:21] previous decade. One 87-year-old [0:23] conjecture from a list of the hardest [0:25] problems of the 21st century got [0:27] disproven during the World Cup final. [0:29] Another 30-year-old graph theory [0:31] conjecture fell to four prompts in 58 [0:33] words. The things have gotten so bad [0:35] that Terence Tao, a man who won an [0:37] International Math Olympiad medal at age [0:39] 10 while the rest of us were making [0:41] cinnamon sugar sandwiches and watching [0:43] Rocket Power, stood up at the [0:45] International Congress of Mathematicians [0:47] and warned of a crisis in the [0:49] foundations of mathematical values and [0:51] practices. In today's video, we'll look [0:53] back at the summer mathematics fell to [0:55] machines and find out what that may mean [0:57] for the rest of us. It is August 19th, [0:59] 2026 and you're watching The Code [1:01] Report. This whole AI doing math thing [1:03] started about a year ago when some [1:05] models solved five of the six problems [1:08] at the International Math Olympiad. But, [1:10] at the time, it felt mostly harmless [1:12] because competition math is the lead [1:14] code of math problems. Then back in May, [1:16] an OpenAI model disproved an 80-year-old [1:19] Erdos Erdős conjecture about unit [1:21] distances and suddenly it didn't feel so [1:23] harmless anymore. [1:24] >> Couldn't believe it. I I had trouble [1:26] sleeping for the first couple of nights [1:27] I went out. [1:28] >> In June, 16 researchers from 15 [1:31] universities published what they called [1:33] the Leiden Declaration, which politely [1:35] asked the world to establish some [1:36] guardrails around AI and mathematics [1:39] research, which the world then politely [1:41] ignored. And last month, while Americans [1:43] were pretending to like soccer and [1:45] Europeans were pretending to like [1:46] medieval infrastructure without air [1:48] conditioning, mathematician Levent [1:50] Alpoge posted a counterexample to X that [1:53] disproved the Jacobian conjecture, which [1:55] is one of the most famous problems in [1:57] algebraic geometry. The idea is that if [1:59] you have a polynomial function whose [2:01] derivative checks out at every single [2:03] point, meaning it's perfectly reversible [2:05] anywhere you zoom in, then the entire [2:06] function should be reversible, too. Now, [2:09] I know that probably doesn't mean much [2:10] to you, but since 1939, that felt so [2:13] obviously true to mathematicians that it [2:15] made Smale's list of the hardest [2:17] problems of the 21st century because [2:19] nobody could actually prove or disprove [2:21] it. That is until Levent did last month [2:23] with some help from Fabel. And just 2 [2:25] days later, it happened again with a [2:27] 30-year-old graph theory problem called [2:29] the dense Garg-Gommans conjecture, which [2:32] you can think of like a delivery routing [2:33] problem. If shipments are allowed to [2:35] split across multiple routes, the [2:37] question is whether you can always [2:38] bundle them into single unsplit routes [2:40] without the total delivery cost going [2:42] up. And for 30 years, everyone assumed [2:44] that you could, they just couldn't prove [2:46] it. Then a researcher named Dimitri [2:48] Rybin pointed GPT-5.6 at it and [2:51] basically told it to make a [2:53] breakthrough. The model responded with a [2:55] tiny network of just seven nodes and [2:57] nine edges where forcing every shipment [2:59] into a single route was always more [3:01] expensive than letting them split, [3:03] disproving the conjecture. And it's not [3:05] just the pros doing this. That same [3:07] week, a Columbia PhD student knocked out [3:09] six open Edges problems in 5 days, and a [3:12] 23-year-old amateur banged out another. [3:14] And this is mostly before any of the big [3:16] tech labs took their own shots. But then [3:18] just 2 weeks ago, OpenAI got in on the [3:21] bullying when they revealed that [3:22] internally their next major model solved [3:25] 10 open problems across math and [3:26] theoretical computer science, and they [3:28] even shipped all of them to GitHub with [3:30] a lean certificate, which is a formal [3:32] proof the compiler can check [3:34] mechanically. The most famous one on the [3:35] list is one I know some of you have [3:37] thought about a lot, which is how [3:38] tightly you can cram identical-sized [3:40] balls into a space. The general bound on [3:42] this problem hasn't moved since 1978, [3:45] but OpenAI just improved it. The other [3:47] nine problems include things like the [3:49] first explicit construction of a [3:51] non-Saugus group and a disproof of [3:53] Connes' rigidity conjecture, which I [3:54] won't pretend to understand, but [3:56] mathematicians have been chasing some of [3:58] them since the '90s. But, of course, [4:00] Dario couldn't just sit by and get big [4:02] derivative by Sam. And so, just last [4:04] week, Anthropic fired back by announcing [4:06] that one of its own unreleased models [4:08] made progress on the Riemann hypothesis, [4:10] which is one of the most famous unsolved [4:12] problems in all of mathematics. It's a [4:14] 167-year-old [4:16] question about the distribution of prime [4:18] numbers, and it's one of the seven [4:20] Millennium Prize Problems with a literal [4:22] million-dollar bounty on its head. The [4:24] best part is that it wasn't an Anthropic [4:26] mathematician who discovered it. It was [4:27] Jared Sumner, the creator of Bun JS, as [4:30] he was on his jog for his I'm filthy [4:32] rich now and need to get fit, too, era. [4:34] During his run, Jared asked Claude to [4:36] take a real stab at proving it, and so [4:38] it did and generated 650 wrong ideas for [4:41] solving the problem. Jared then told it [4:43] to try again, and this time the model [4:45] spent a day and a half coordinating 60 [4:48] sub-agents inside Claude code, running [4:50] 2,400 shell commands, writing hundreds [4:52] of Python scripts, and burning 31 [4:54] million output tokens. Now, that still [4:56] didn't lead to it proving the [4:57] hypothesis, but it did bump the fraction [5:00] of solutions that probably satisfy the [5:01] hypothesis from 41% to 67%, which I'm [5:05] told is pretty groundbreaking. The [5:07] result was validated by two [5:08] mathematicians at Anthropic, and checked [5:10] by two outside number theory experts, [5:12] and formalized in Lean. We live in crazy [5:14] times, but stuff like this wouldn't be [5:16] possible without amazing cloud providers [5:18] like Railway, the sponsor of today's [5:20] video. They once again refused to waste [5:22] your time with a full ad, and you can [5:24] say thank you by checking them out for [5:26] your next project at the link below. [5:27] This has been the Code Report. Thanks [5:29] for watching, and I will see you in the [5:31] next one.