LucentFire · a BenevolentSky LLC service

Reports

Checks of public technical claims. What we ran, what it showed, what it does not settle — and the commands to run it yourself.

12 September 2026 · Lean formalization

We rebuilt OpenAI's Navier–Stokes proof on a desktop

11,424 build jobs, exit code 0, thirty-eight minutes. No unproven gaps in the proof path and no added axioms. The theorem lets the construction choose the external force — Clay alternatives (C) and (D) — which is narrower than the headlines and exactly what OpenAI's own README says.

Build passes No gaps Standard axioms Narrower than reported

How a report here works

We check artifacts, not reputations. A claim with something released — code, a formal proof, a dataset — can be checked by anyone. We do that and publish what came back.
Every report names what it does not settle. A build proves a build. It does not prove the statement means what its author intended.
Reproduction steps are on the page. If you cannot repeat it, we have not shown you anything.
Our own misses get published at the same brightness as everything else.