The same arithmetic as the reports, running in the browser. Of the 23 instruments, ten run a battery in the test suite, one draws its headline number from a certificate the reports also read, nineteen decide it in exact integer or rational arithmetic, and three are floats and say so beside the number. None of these pages is a report: nothing here carries a verdict a build would refuse to publish, and every card below says what backs its headline number.
Nothing here is a perfect circle
The elicited geometries look like they hold shapes — a pentagon here, four points on a circle there. So this looks exhaustively, at every triple and quadruple and five-subset of every set from every model, and then runs the identical search on the same numbers with the geometry shuffled out. Almost nothing survives that. What does is not a polygon — and for most of the sets the verdict is not a margin at all but a certificate in whole numbers that no such points exist.
read the hunt →Turn the singularity
A Millennium proof says a smooth force can drive a fluid from rest to infinite speed in finite time. Everyone else will render a simulation of that; a simulation is the one thing here nobody can certify, so this draws the object the proof constructs instead — a core that collapses as you move time, its aspect ratio diverging. One dial is the smallness parameter the whole argument hangs on. Move it and two classical exclusions close on it from opposite sides, each verdict an exact rational inequality decided in integers as you drag.
open the instrument →Not the picture. The set of pictures
The famous black-hole image is one sky chosen, by an imaging prior, from the infinitely many the data allow. This draws the set instead: 18 skies fitted under deliberately different priors, agreement rendered as ink and disagreement as texture. One slider decides how much of the phase information the picture is allowed to use — and at zero the ring dissolves, because amplitudes alone cannot see where anything is.
open the instrument →The line they published, and the lines that fit
A calibration is run forwards and used backwards, and the backwards number always comes off a fitted curve. The fit is an assumption and it is never priced. This computes what the standards allow instead — in closed form, no optimiser, no sampling — under assumptions you can dial one at a time, from monotone only to join the dots, with the parametric fit past the end of the dial.
turn the dial →Manifolds we are handed
Their manifolds are found — pulled out of a working model and interpreted. These are stated: a rule, its parameters, and then a drawing. Two of the eight are not illustrations at all but certificates rendered at their own resolution, which is what a proof looks like when you stop reading it and start looking at it.
open the series →The geometry of feeling, and the control that catches it
Twelve feelings, then the same twelve asked again under six moods — and twelve clock hours carried through the identical pipeline as a control that has no business moving. A mood effect that also moves the clock is not a mood effect. One model’s clock moves anyway.
read the moods →The shape of an answer
Ask how different two things are, one pair at a time, and you get a table of numbers. A table of distances is a shape — or it is not one, and the difference is decidable in exact integer arithmetic. Every pair is asked both ways round, so the asymmetry is measured rather than averaged away.
compare the three →The shapes a model will admit to from the outside
Goodfire finds circles and colour surfaces by opening the model and decomposing its activations, which needs the weights. This asks from outside instead — every pair, one integer, one row at a time — and then decides exactly what those answers can be. If the circle is real it should survive being asked about; a shape that lives only in the activations was never a shape the model uses.
read the plates →Point it at something whose shape is already known
Every other geometry page here asks a model for a table of dissimilarities and decides what shape the answers have. This one asks nothing. The prediction is written first, in the source, and never edited afterwards — which is the only thing that makes “agreed” mean anything.
read the controls →The rule is a wire you cannot draw
Every verifier has rules about what may decide what, and they are almost always prose in a README. Here two of them are conditions on a connection: a value that came from floating point has no wire into a port that decides. Break it and nothing scores badly — it does not build, and what comes back is the sentence the engine raised. Drag the forbidden wire and the engine answers you itself.
wire it wrong →Fourteen million verdicts could not see it
One mutant of a comparator, or the unmutated design. Name the input pair whose pins differ, or prove there is none — kills verified by simulating the netlist, equivalence by SAT, no answer key.
Decide it, or say what is missing
An environment built out of a grader bug. Three models, 135 rollouts, one dial: how much of the reference is stated — every quantity, a norm printed as a whole number, or a quantity missing. The grader is exact and the answer it exists to train against is the confident verdict on a task with a hole in it. Ten forgeries were planted before any model was called; all ten are caught, at every build.
read the environment →Rewire it yourself
24 lattice claims with exact answers and three graders. Only one may reach the socket that decides. Drag a different one onto it and the engine refuses in its own words; drag it onto the socket that only reports and the admitted count moves in front of you — the tolerance grader admits 17 where the exact predicate admits 12, because past dimension 102 the determinant is Infinity to a double.
rewire it →Solid where it was proved
Lattice security rests on how short a vector can be found, and the SVP challenge publishes 926 records as six-figure floats with no error bound, all pressed against one wall at 1.05 times the Gaussian heuristic. 37 of them are decided here in exact arithmetic — π bracketed, the determinant read from the basis, the predicate raised to the n-th power in integers. None is inconsistent with its printed norm, and exactly one cannot be decided from it. Audit only; nothing here proposes a primitive.
watch the reduction →The occultation, without the ellipse
A star winks out behind a small body and 5 telescopes each measure one chord across its silhouette; 23 more saw nothing. Every published size is an ellipse fitted to the chords. This asks what the chords force on their own, assuming only that the silhouette is convex — and the answer is closed form: the diameter sits in [168.3, 267.5] km, the published 206 ± 15 inside it, and the stations that saw nothing are worth 309 km of ceiling. Every area an exact rational; nothing converges.
read the bracket →How far can two cameras bound a wave?
A stereo-video rig recovers the sea surface from the pixel offset between two images, and every pixel is a box. The set of elevations the rig cannot tell apart at a range is a cell computed here exactly, in interval arithmetic, over inputs that may themselves be boxes — a pixel pitch the paper does not state. Turn the baseline, the lens, the lag, the sea; read the bound at any range and the range at which it first exceeds a tolerance. Preset: the two-smartphone rig of Vieira, Guimarães et al. (2020), whose observed error against a pressure gauge lands inside the budget its own numbers give.
turn the rig →Every cell a certificate
Reis, Guimarães et al. (2026) map, over the ocean, which of six families fits significant wave height best and the 100- and 1000-year wave it implies. Here is that map on the paper’s own hindcast with every cell certified — the choice DECIDED or REFUSED, never guessed — the paper’s regional claims decided as boxes, a seventh family (the GEV) beside the six, the width another 32 years could give each number drawn apart as statistical, and a globe you can turn to any cell and certify again in your own tab, from the pinned data, with the same code.
turn the globe →Price the bond the Treasury’s way, to the last truncation
Tesouro Direto publishes a price for every bond every day and the Treasury publishes the formula, down to which step is truncated at how many decimals. This page runs that formula exactly in your tab — a rate, a settlement date, a maturity — and shows the enclosure of the one step that is irrational and every truncation as a decision. Paste rows of the published file and each gets the verdict the report gives it: reproduced, off by so many centavos, or refused.
price a bond →Certify a return level. Your file never leaves this page
An offshore design value is read off a distribution fitted to wave heights, and the fit is usually wherever an optimiser stopped. Drop a record — or take the Campos Basin hindcast — declare the block, and the six families of Reis, Guimarães et al. (2026) are fitted and certified in your tab by the code that certified the return-level report: every fit a box proved to hold one maximum of the likelihood or a refusal, four criteria and the 100- and 1000-year levels as enclosures, the choice DECIDED or REFUSED, and a certificate to download that carries your file’s sha256, never the data. A second panel decides a fit someone printed: reproduced, off the maximum, or outside its own support.
certify a record →Every hour of sea, against every contour
An environmental contour is the line an offshore designer reads a fifty-year sea state off. Nine groups drew theirs for six metocean datasets in one benchmarking exercise, scored by counting the hourly observations outside each. Every contour drawn over the 1,840,824 hours it was scored on, the count re-decided exactly — 173 of 176 printed numbers reproduce, 30 of 150 contours cross themselves — and any sea state you click decided INSIDE, OUTSIDE or ON by the code that decided the ledger.
decide a sea state →Unique totals, and the split nobody can see
Two populations pay the same price per edge, so the equilibrium fixes every total and not whose flow it is. The set of splits it cannot tell apart is a face; its dimension is decided in exact rationals in your tab — 6 on the published network — and a drag moves the split while every total holds. Backed by: the face law over 3,925 networks, the engine cross-checked against its record at build.
pull on the split →The transit, without a law for the star
Every published planet radius is a statement about a star’s atmosphere as much as about a planet: how much light sits where the planet passes is decided by a limb-darkening law nobody measured for that star. This asks what the photometry forces on its own — the star is any nonnegative brightness profile at all — and the answer is one-sided: the data bound the planet tightly from below and the whole upper bound is bought by the assumption. 29 published values across 2 planets, all inside; nothing in the optimiser is trusted.
read the enclosure →An attention row is a point. Nobody draws it that way
Attention weights are nonnegative and sum to one, which makes a row a point in a simplex — and a bar chart throws that away. Focus is distance from the centre; concentration has contours; temperature is a path. One real row from a tiny GPT, in the room it actually lives in, with the one claim about it that is decided rather than drawn: sharpening must move the point toward a vertex, proved in exact rational arithmetic because consecutive values differ in the fourteenth decimal.
open the instrument →