The 62-Page Failure Log Behind Astra's 10 Proofs

A 62-Page Document Cataloging Only Failed Approaches Came With It

On August 1, OpenAI announced that an internal version of its next model, Astra, had solved 10 unsolved problems in mathematics and theoretical computer science. What caught the attention of Korean media was a figure of about ₩2,890,000 (~$2,000). That number came from converting the tokens OpenAI spent to find the solutions into dollars at Sol API rates—roughly $2,000—and then translating that figure into won. It doesn’t represent the total research cost, including model development and human review.

But that day didn’t produce just one document. There was a 249-page paper laying out the results, a repository of machine-verified formal proofs, and one more document—62 pages long. Its title: “How the Ideas Came Together.”

Reader, open this document and it feels a bit strange. There’s not much talk of correct answers. Instead, it keeps circling back to “why this approach didn’t work.”

What’s actually new in this announcement isn’t the fact that AI found the answers—it’s that OpenAI compiled and published, as a separate document, every approach it discarded along the way.

First, What Are These 10 Problems?

You don’t need to understand the content in full — just get a rough sense of what kind of problem each one is.

#	Problem	In plain terms
1	High-dimensional sphere packing	How densely can you pack spheres together?
2	Binary and spherical codes	How many error-tolerant codes can you build, at most?
3	Non-sofic groups	Are there infinite symmetric structures that can’t be approximated by any finite shuffling?
4	Connes rigidity conjecture	Can a structure be reconstructed just from its shadow?
5	Arithmetic circuit complexity	What’s the minimum number of multiplications a given computation requires?
6	Quantum parallel repetition	Does playing the same game repeatedly make the odds of winning drop sharply?
7	Closest vector problem	How hard is it to find the nearest point in a lattice?
8	Ehrhart volume conjecture	What’s the maximum volume a shape satisfying certain conditions can have?
9	Multicolor Ramsey numbers	No matter how many colors you use, do you eventually end up with a same-colored triangle?
10	Extremal graph theory	How many lines can you draw at most while still avoiding a specific shape?

Problems 3 and 4 had been open since 1999 and the 1980s, respectively, while 9 and 10 correspond to numbers 183, 146, and 180 on the list of open problems left by Paul Erdős, the Hungarian mathematician. The answers also come in different flavors: some are brand-new proofs, others are counterexamples that demolished conjectures long assumed to be true.

cdn.openai.comcdn.openai.com

One small fact worth flagging here: OpenAI counts the results as 10, but the walkthrough document actually has 12 chapters. That’s because problem 5 splits into circuits and formulas, and problem 10 splits into two separate extremal-graph-theory papers. Even the formal-proof repository bundles its 12 endpoints into 10 “results.” It’s not a major issue, but it’s worth remembering that “10” isn’t a natural unit here — it’s an edited one.

What the Walkthrough Actually Shows

As I counted while reading through the 62-page document, 10 of the 12 chapters open with a story of a failed approach. Even the chapter titles say so: “Why the First Recurrence Was Wrong,” “The Long, Useful, Failed Path,” “Why the Obvious Reduction Couldn’t Work.”

The shapes of failure differ. Let me break them into four types.

Type 1: A Plausible Analogy That Was Wrong

Chapter 2, the error-correcting code problem.

The model borrowed a formula it had used for a different problem with a similar structure and applied it. The form looked right. But then it tested the formula on a tiny case: a length-8 code.

The formula’s upper bound came out to 508 divided by 7, roughly 72.6. But that code actually has 128 valid instances. In effect, the model had said “at most 72” about something that has 128.

This isn’t the kind of thing you can wave away as a rounding error. If the upper bound comes out smaller than the actual value, something is structurally wrong with the calculation. The document is blunt about it: this wasn’t a harmless normalization issue — it exposed a structural error.

Recalculating with the corrected formula gave about 261.8. That’s greater than 128. Now it makes sense.

What’s striking isn’t that the formula got fixed — it’s that the model found and tested, on its own, the smallest possible case that could reveal whether its idea was wrong.

Type 2: A Shortcut That Breaks the Very Condition It’s Supposed to Satisfy

Chapter 10, the Ramsey number problem. The goal is to color things so that no same-colored triangle appears.

The model came up with a shortcut. Using permutations, you can generate k-factorial points from k colors. With 10 colors, that’s 3,600,000 points — remarkably efficient.

But on checking, it turned out that under this scheme, three permutations could send the same position to three different places. And those three positions formed exactly the same-colored triangle the whole construction was meant to avoid. The structure produced precisely the thing it was supposed to prevent.

Something similar happens in Chapter 5. While trying to prove a lower bound on computational cost, the model added a correction term to each item — but the number of multiplications that correction itself required turned out to equal the very number of multiplications the proof was trying to establish. The structure just fed the target quantity back into itself, so nothing new got proven.

Type 3: Proving That a Direction Cannot Work

Chapter 1, sphere packing. This is the most interesting one.

The model approached the goal using a standard inequality, but stalled at roughly half of the target value. The usual instinct here is to think, “I just need to tighten the constant.”

The model did something else. It showed, via a counterexample, that this direction could never reach the target value at all. The document’s diagnosis: this wasn’t a matter of an under-optimized constant. A tool that only measures overall size forgets where, specifically, the problem lies.

It wasn’t simply stuck — it had proven that the target was unreachable from this direction. So instead of tightening the constant, the model switched tools entirely, and that’s when progress resumed.

This distinction matters a lot in practice, too. “Not there yet” and “this direction won’t get you there” call for completely different next moves.

Type 4: Finished, Then Discarded

Chapter 8, the closest vector problem, connected to lattice-based cryptography. Here the model completed a full proof — and then threw the path away.

The model approached the problem using signed histograms over a prime field and completed the proof to the end. The document explicitly states that this path provides a complete construction — meaning: it worked.

But that’s not what made it into the final version. What appears there instead is a version rebuilt in characteristic 2, where addition reduces to pure parity arithmetic. The signed histogram became an odd/even table; complicated cancellations became parity checks. Same conclusion, far fewer moving parts.

Chapter 9 devotes an entire section outright to a failure — titled “The Long, Useful, Failed Path.” That path found precisely the right shape for the answer. But it couldn’t explain the factorial attached to that shape’s volume. The model got the answer right without being able to say why. The document classifies this as a failure — but a useful one, since it revealed why the factorial was necessary in the first place.

There’s a better moment in the same chapter. Partway through, the model writes that there’s a strong temptation to treat two functions as identical. It immediately produces a counterexample showing why they must not be treated as identical — and adds that doing so would have built the proof on a false identification.

Chapter 12 is honest from the start. The section’s opening line reads: “We initially tried to find a proof.” And the chapter ends with a counterexample — meaning it began without even knowing whether the statement was true or false.

So how far do these results actually apply

When I look at claims about achievements, I tend to check the scope first. What the result actually applies to determines what it actually means.

A lot of domestic coverage connected the closest vector problem to post-quantum cryptography. The direction is right. But look at the dimension the result covers: it’s the input size to the 401st power. The 401st power doesn’t give you an intuitive feel, but even with an input of 10, that’s a 1 followed by 401 zeros. The number of atoms in the universe is about a 1 followed by 80 zeros. The walkthrough doesn’t hide this—it states it directly. This claim is about polynomial-time computability, not practical efficiency. It’s not an attack on the cryptography we currently use.

The 9th Ramsey result is similar. For the newly obtained lower bound to have meaning, the number of colors needs to be 342 or more. Below that, the previously known trivial lower bound is actually stronger. The 5th circuit lower bound only holds once matrix size is 65,000 or larger.

Formal verification is the same story. OpenAI stated that all results were formalized in Lean¹, with no incomplete goals, using only standard axioms. That’s strong grounds. However, the review status the repository lists is “agent-reviewed.” And what a machine verifies is the logical derivation—not whether the formalized proposition is the same proposition as the original problem. That comparison still falls to humans, and it hasn’t been peer-reviewed yet.

British mathematician Thomas Bloom reacted to the announcement by calling it “phenomenal news.” Terence Tao, on the other hand, has had a different worry for a while now. AI-generated proofs are piling up fast, but the pace at which people can understand and accept them can’t keep up—a state he’s called proof indigestion.

These two reactions aren’t contradictory. Whether a result is real and whether the academic community has understood and accepted it are two separate things. That’s exactly the point the Leiden Declaration², endorsed by the International Mathematical Union on June 2nd, was addressing: verifiability, sourcing, and honest documentation of who did what.

In that light, one sentence in OpenAI’s announcement is worth noting: attaching a human author to a proof that was entirely AI-generated distorts both the system’s contribution and the human intellectual work. It’s not common for a company to voluntarily disclaim its own share of authorship.

Oswarld’s Lens

I think the most valuable output of this presentation is a 62-page document cataloging failed approaches.

There’s a scene I run into every time I do a GTM strategy project. The final deliverable is a single page of recommendations. But more than 70% of the actual working time goes into filtering out, one by one, the candidate approaches that never make it onto that page. Why this channel doesn’t work. Where this pricing structure breaks down. Why hitting this segment first blocks the next stage.

The problem is that 70% never survives into the document. Options that were reviewed and rejected either get pushed into an appendix or dropped entirely. Nobody asks about them in the presentation room. So here’s what happens: six months later, a different team brings back the exact same idea as something new. The organization ends up re-examining, from scratch, an option it had already ruled out. I’ve watched this scene play out at multiple companies, and I keep arriving at the same conclusion — an organization’s real asset isn’t the approach it adopted, but the reasoning behind the approaches it discarded.

What makes this presentation interesting is that it reverses the convention of only publishing successful outcomes. If you show only success, you can’t answer the question “wasn’t that just a lucky guess?” But if you also disclose which approaches were abandoned and why, readers can trace what judgments were made, and in what order. That becomes the basis for trust.

One more thing. I’ve long been uncomfortable with the market for content that packages only success stories. That kind of content always builds its narrative backward from the outcome. This document doesn’t do that. Because the discarded approaches remain as a list, readers can examine that judgment for themselves. I think this format should become the standard for how AI-driven performance claims get presented across the board.

Let me be clear about one thing, though: this document is not a record of the actual thought process as it happened. It’s a narrative reconstructed by a separate AI model that read both the original logs and the final paper together. Any story assembled after the fact inevitably picks up a bias toward looking smoother than reality was. So this document is less a lab notebook written in the moment and more a well-organized retrospective written later. Still, that’s far better than having no such account at all.

Closing

Let me sum this up in three lines.

1. Alongside the paper with the actual answer, there’s a companion 62-page document cataloging the approaches they tried and discarded. 10 of its 12 chapters start from a failed approach.
2. The failures fall into four types: a plausible analogy that turned out wrong, a shortcut that broke the target condition itself, a proof that a given direction simply wouldn’t work, and a completed proof that got discarded anyway.
3. You have to look at the conditions each result actually covers. The nearest-vector result applies to dimensions on the order of the input size to the 401st power, while the Ramsey lower bound and the circuit lower bound hold only under conditions of 342 or more colors and matrix sizes of 65,000 or more, respectively. An increase in problem-solving capability is not the same thing as immediate applicability to the technology we use today.

After reading this, I’d suggest trying just one thing. If you made a decision this week, jot down two lines next to the option you chose: the option you discarded, and why. Six months from now, those two lines will save you a full hour of meeting time.

Does your organization actually keep records of “we reviewed it but it doesn’t work”? If you do, tell me in the comments what format you use. If you don’t, tell me where the process breaks down. Once enough cases come in, I’ll turn them into a practical format for logging discarded options in a future issue.

---

💬 If you have a way of recording discarded options, share it in the comments

📨 If you have a colleague reviewing the same conclusion twice, forward this piece to them

---

References & Further Reading

Primary sources

• OpenAI, “Ten advances in mathematics and theoretical computer science,” August 1, 2026. Link ··· This is the original document listing the 10 results along with OpenAI’s stance on authorship. I’d recommend reading at least the final section, “Responsibility to the Mathematical Community,” yourself.
• OpenAI, How the Ideas Came Together, 62 pages, August 1, 2026. Link ··· This is the core evidence behind today’s piece. Skip the equations and just skim the first two subsection titles of each chapter — the nature of this document becomes immediately clear.
• OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, 249 pages. Link ··· This is the body of the results. Check the dimensional calculation at the end of Chapter 8 — the question of effective scope becomes much more concrete there.
• OpenAI, “ten-proofs” formal proof repository, GitHub. Link ··· The 10 results are broken down into 12 formal endpoints here. It’s worth checking the review-status labels yourself.

Background

• Leiden Declaration on Artificial Intelligence and Mathematics, June 2, 2026. Link ··· This is a declaration endorsed by the International Mathematical Union. More than 1,000 people signed it within 24 hours of its release. I’d recommend reading it first as background for this issue.
• Henry Cohn and Noam Elkies, “New upper bounds on sphere packings. I,” Annals of Mathematics 157 (2003), 689–714. Link ··· This 2003 paper set the threshold that Result 1 reaches. Reading Sections 1 and 2 helps situate where this new result stands.

---

The author is Oswarld (Kwangseob Ahn). Current roles: Adjunct Professor at Sejong University, Strategy Consultant at INLEVEL9. Career, research, books, and recent work are kept current on the About page. Latest · July 2026: HEMA-2: A Consolidation-Aware Tri-Memory Architecture with Multi-Channel Scheduling for Lifelong Conversational AI.

📝 Glossary

Footnotes

1. Lean: A language for writing mathematical proofs in a form a computer can check line by line. Instead of a human judging “this looks right,” the machine automatically catches logical gaps. That said, it checks the logical derivation only — whether the stated proposition is actually the same as the original problem still requires human judgment. ↩

2. The Leiden Declaration: An international statement on the relationship between AI and mathematics, released June 2, 2026. It grew out of a workshop held in Leiden, the Netherlands, in September 2025, and was endorsed by the International Mathematical Union. Rather than banning AI use, it calls for verifiability, source disclosure, and research autonomy. ↩