In the 1600s, Prince Rupert of the Rhine won a wager that sounds impossible: you can cut a straight hole through a cube large enough to pass a second, equally-sized cube clean through it. A shape where a copy of itself can be slid through a straight tunnel bored in it is called Rupert. Over the following centuries every Platonic solid, and almost every Archimedean one, was shown to be Rupert. It became natural to conjecture that every convex polyhedron is Rupert.
Last year, the first ever counterexample was proven: the "Noperthedron," a bespoke 90-vertex solid whose proof leaned essentially on the shape's central symmetry. It's not Rupert, or "nopert" as they say.
Today, we're proud to announce the Omniscience Research Agent has proven the second nopert shape ever: the stellated tetrahedron P11/20.
An 8-vertex holdout
The shape is a stellated tetrahedron: take a tetrahedron, glue on a shrunk-and-flipped copy of itself scaled by a factor of 11/20, and take the convex hull. The result has just eight vertices. A mathematician (Tony Zeng) conjectured it is not Rupert, and pinpointed exactly why the existing techniques could not finish the job: this solid is not centrally symmetric. The symmetry that made the Noperthedron tractable is gone, and with it goes the trick that lets you ignore the sideways shift. What was missing, in Zeng's words, was "a local theorem that accounts for the translation term."
That is the theorem the agent set out to build.
What the agent actually did
Proving a shape is nopert means proving that no shadow of the solid can be strictly contained inside another shadow of it, over a continuous, high-dimensional space of two independent rotations plus a two-dimensional translation. You cannot check that space point by point because it is infinite. The agent's strategy was to reduce the whole infinite problem to four finite, certified computations, each covering one regime of the configuration space, glued together so that no configuration can slip through a gap between them:
- a cylinder / box certificate that excludes a neighborhood of near-aligned rotations for every translation;
- a second-order stress certificate controlling the critical directions where the shadows almost fit;
- a depth grid proving the shadow has strictly positive "slack" away from those critical windows;
- a far manifold that kills every remaining rotation far from alignment.
All four are carried out in outward-rounded interval arithmetic. Every number is a rigorously
enclosed range, never a rounded float, so that a machine can certify each cell without any appeal
to trust. Assembled, they cover the entire space. A single top-level verifier reads the four
certificates and reports one word: COMPLETE.
Measured twice, proven once
A proof you cannot check is a rumor. So every certificate the agent generated is re-checked by an independent replay verifier that shares only the interval-arithmetic core with the generator, not the search logic that found the certificates. The verifiers confirm exhaustively that the certified cells cover the space with nothing missing, tile it exactly with no overlaps, and, cell by cell, across all of the millions of them, that each stored certificate genuinely re-certifies. The far-manifold recovery layer alone was re-executed in full: every one of 1,038,991 cells, zero bad.
And it is all open. The complete code is on GitHub, and the roughly two gigabytes of certificate data are
hosted publicly. Anyone can download it and watch their own machine print COMPLETE.
That is the standard the great computer-assisted proofs are held to, and this one meets it.
Why this matters
Step back from the geometry for a moment. Mathematicians for years studied Rupert polyhedra, but only one nopert ever proven. What's new is AI mathematical research: developing new local theory, inventing soundness lemmas needed to dodge a genuine ill-conditioning barrier, architecting a four-part certificate, and actually seeing it through to completion.
Furthermore, this theory and technique appear useful to prove additional nopert polyhedra going forward. The Omniscience Research Agent did not just solve one problem. It opened a path that future mathematicians (whether human, AI-human centaur hybrid, or autonomous AI) can follow to get more even results.
The Omniscience Research Agent did that hard work. It's been designed as an AI researcher capable of solving the world's hardest problems. This is one such problem. There are thousands more where the missing step is a tireless, rigorous, and genuinely creative researcher who never loses the thread. Importantly, it doesn't just do math, but science too, or really any research that involves thinking really hard, reading the literature, trying things, and producing significant results.
That is what we are building. Does your field or organization have hard theoretical problems it needs solving? Talk to us.