OpenAI shipped Lean 4 proofs. That is the same idea we enforce at runtime.

What OpenAI published

On 1 August 2026, OpenAI announced ten results in mathematics and theoretical computer science, each resolving or advancing a problem that had been open for years. The work spans sphere packing, coding theory, group theory, operator algebras, quantum complexity and extremal combinatorics.

The interesting part is not the headline. AI systems have claimed hard mathematical results before, and some of those claims did not survive review. What changed here is the evidence. OpenAI released a public repository, openai/ten-proofs, containing Lean 4 formalisations of every result under an Apache 2.0 licence.

The repository has a sorry count of zero. In Lean, sorry is the placeholder that lets a proof compile with a gap in it. Zero means no step was skipped or asserted without justification. Anyone can install Lean 4, build the repository, and check every claim against the kernel's logical axioms. Nobody has to trust the model, the lab, or the press release.

Why that matters beyond mathematics

This is the difference between a claim and a certificate. A claim asks for confidence. A certificate can be re-checked by a third party who trusts none of the parties involved.

Formal methods have carried this weight in high assurance engineering for decades: avionics, chip design, cryptographic protocols. What is new is the pairing. A model explores the space and proposes, a formal system checks. Creativity from one side, certainty from the other.

• The proposer can be brilliant and still be wrong. That is fine, because it is not the authority.
• The checker is narrow, mechanical and repeatable. That is exactly what makes it trustworthy.
• Verification cost is small relative to the cost of being wrong.

The same shape as agent security

Glio is built on the same foundation: mathematical reasoning and formal logic, expressed in Lean 4. Instead of certifying a theorem, we certify an action.

An agent reasons and proposes a tool call. Glio checks that proposed action against your formalised policy before it executes. Permitted actions pass. Forbidden actions never happen. The verdict is deterministic, so the same action against the same policy returns the same answer every time, with a proof behind it, in milliseconds and in the hot path.

Most agent security is probabilistic. A model watches a model, scores risk, and catches most of it. Most is a difficult word to bring to a risk committee. A proof is not a confidence score, and it does not degrade when the agent is jailbroken, manipulated or simply wrong. Enforcement sits outside the model's reach, and fails closed by default.

OpenAI's repository makes a mathematical claim independently checkable. Glio makes a safety claim independently checkable. Same technology, applied to the moment an agent stops reasoning and starts doing something real.