OpenAI's unreleased Astra model produces new hardness result for lattice cryptography

OpenAI published ten new results in mathematics and theoretical computer science on 1 August 2026, attributing the mathematical arguments to an internal version of Astra, which it describes as its next major model.

One of the ten sits directly on the foundations of post-quantum cryptography.

The lattice result

Result seven concerns the closest vector problem, or CVP. Given a lattice, which is a regular grid of points extending through high-dimensional space, and a target point that does not sit on the grid, CVP asks which grid point lies nearest to it. The problem is straightforward to state and, in high dimensions, extremely difficult to solve.

That difficulty is the point. The security of lattice-based encryption rests on the assumption that problems of this kind cannot be solved efficiently, including by a quantum computer. Lattice schemes are the basis of the algorithms now being standardised and deployed for post-quantum migration.

According to the published paper, the model produced a direct reduction from 3SAT establishing hardness for the Euclidean closest vector problem to within a factor of n to the power of one four-hundredth, with related consequences for binary decoding and for lattice problems in other norms. OpenAI's summary describes the result as polynomial-factor hardness of approximation for CVP, and calls it a foundational lattice question related to post-quantum cryptography.

The direction of that result matters and is easy to misread. This is a hardness result. It is a proof that the problem is difficult, not a method for solving it. Nothing in OpenAI's publication describes an attack on any cryptographic scheme, and no deployed algorithm is affected. Results of this type strengthen the theoretical case that the problem is intractable rather than weakening it.

Two caveats belong alongside it. Hardness of approximation results concern worst-case instances, while cryptographic security depends on the difficulty of the average case, so a worst-case result does not transfer directly into a security guarantee for a deployed scheme. And the result itself has not yet been through the normal process of specialist review.

What verification has and has not established

OpenAI says the model formalised each argument as a Lean certificate, with the files published on GitHub. Lean is a proof assistant that checks whether each step of an argument follows from its stated definitions and assumptions.

This is a meaningful form of evidence. Anyone with the Lean compiler can check the certificates without trusting OpenAI. It closes off the failure mode where a plausible-sounding argument conceals a gap.

It does not settle everything. A Lean certificate confirms that a formal statement follows from its premises. Specialists must still confirm that the formalised statement is the statement the mathematical community actually cares about, and assess the result's novelty and significance. That work has not yet happened for any of the ten.

OpenAI is direct about how the results were produced. It says the mathematical arguments were generated by its system, while the company helped prepare the manuscripts and formalise the proofs, and takes responsibility for their correctness. It also acknowledges the concerns of signatories to the Leiden declaration on AI and mathematics, and says claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of human intellectual work.

What is known about Astra

Astra is not publicly available and OpenAI has not announced pricing, access or a release date. The company describes it only as its next major model.

OpenAI says the tokens needed to find solutions to all ten problems would have cost roughly US$2,000 at GPT-5.6 Sol API rates. That figure covers the successful runs. It does not include model development, failed attempts, researcher time or formalisation work.

BleepingComputer reports that OpenAI has not decided whether the model will be released as GPT-5.7, GPT-6 or under another name, and describes Astra as built for long-running workloads, allowing agents to work on separate parts of a larger problem. The Information separately reported that OpenAI is working on the model.

Why it matters beyond mathematics

The other nine results span sphere packing, coding theory, group theory, operator algebras, arithmetic circuit complexity, quantum complexity and extremal graph theory. All ten address problems OpenAI says have seen no progress on their main result for at least a decade, and in most cases considerably longer.

For security teams, the specific lattice result changes nothing operationally today. The broader signal is worth registering. The mathematical assumptions underpinning post-quantum cryptography are now territory that frontier AI systems are actively working in, and producing publishable results in. That applies to arguments that reinforce those assumptions, as this one does, and in principle to arguments that would test them.