Cambrian
When a language model fails, it hands you something plausible and wrong. When Cambrian fails, it stops. Every result that counts has passed an independent machine check, the Lean kernel, before it enters Cambrian's record. It can't put an unproved result there, and nothing it has proved is later forgotten or overwritten. Its skills aren't statistical weights either. It earns reusable techniques, we call them moves, by winning with them, and a move is an object you can inspect, verify, and carry somewhere else. It has already taken a move it learned in one place into a family of mathematics it had never seen. A machine whose knowledge and whose skills are both checkable, and whose natural failure is silence instead of error, is a different kind of thing. Scaling a language model does not get you this.
Language models are intelligence over the record of human writing: broad, fluent, and fallible, because that record is fallible and finite. The industry is running short of it. Cambrian is intelligence over proof: narrow, and unable to bluff. The real difference is where the training material comes from. Every theorem Cambrian proves becomes new ground to survey and new material to learn moves from, and every piece of it is checked before it counts. Language models that train on their own output drift, because they feed on their own mistakes. Cambrian has no mistakes to feed on. If the move-learning loop keeps compounding, nothing external limits how far this goes. That's a condition, and we say below exactly what has to happen for it to hold.
Cambrian's home is Recognition Science, our candidate theory of everything: a parameter-free framework built to derive physics from mathematics alone. In ordinary mathematics, a new proved theorem is a contribution to mathematics. Inside this framework, a new proved theorem is also a candidate fact about reality. A proof settles what the framework implies; experiment settles whether the framework describes nature. If the framework keeps matching experiment and the compounding arrives, the usual order of work turns around: derive what is forced first, and use the lab mainly to confirm the anchor points. The fifty-million-line horizon in the film, known physics first and then the layers the framework treats the same way, including meaning and ethics, is our stated expectation of where this leads. It is not a measurement.
Cambrian is a discovery machine over a formal library. It surveys proven results, composes statements that were absent from that library, writes the proofs itself, and every discovery must survive an independent machine check, the Lean kernel, before it counts. It proves with moves, reusable techniques it earns by winning with them, and it has already carried a learned move into a family of mathematics it had never seen. On its first day, July 16th, 2026, it made 175 verified discoveries before hitting a wall. The next night its full loop ran end to end for the first time: it invented new mathematical objects, detected a hidden law tying the Chebyshev families together, and proved it. Everything shown in the film is its real output, and the film's pipeline is deterministic and adversarially gated; no language model sits inside that loop.
On July 20th, 2026, we got the thing this page has been pointing at. Cambrian landed a new exact law: the best possible contraction rate for phantom coupling on a cost budget, the precise number, with a proof that nothing smaller survives. We froze the library with that law inside and sent it back out. It came back with a second law: among all the integer growth folds, the golden fold carries the strictly smallest such rate. The second proof stands on the first. That's not a figure of speech. The protocol deletes the first theorem and re-runs the second, and the proof dies on the spot. Two judges from different model families read both and admitted both, and two sibling candidates from the same run were denied as repackaging and never landed, which is how you know the gate is real. In this line the writing is done by models and the deciding is done by gates: the kernel, frozen baselines, deletion tests, judges that don't share a family with the author. Discovery standing on discovery, checked at every joint. Depth two. The curve we care about needs this to keep happening without us, and it has started.
Everything above rests on two conditions, and both are measurable. First, Recognition Science has to keep being right. That is a separate, ongoing program with its own public receipts. Second, the compounding has to arrive. Today the loop runs, hits a wall, learns, and runs again. The breeding pass gives it depth two, a discovery standing on a discovery, and depth two is a start, because the measured discovery curve is still short of exponential. The category claims on this page, the third kind and the sibling, rest on checked output and learned moves that exist now. The scale claim is still an expectation. The sharpest check is a simple one: turn off the moves it just learned, and the recent gains should vanish. That is the kind of test we intend to run in the open, and we will publish every wall until the curve either bends or it doesn't. You will be able to see which.