A machine is composing mathematics with itself right now. Each theorem counted below was conjectured and proved by the machine, and every proof was certified by the Lean kernel, the same referee that checks the human library. Nothing enters the count that the kernel did not accept.
Live status
| Stage | A: the frontier |
| Library processed | about 16.2h of frontier remain |
| In the pipe (conjectured or awaiting banking) | 8,649 |
| New mathematics still growing | yes |
| No padding with duplicates | holding |
| Failures nominal | yes |
The wave
Each bar is one slice of the library. Its height is the share of newly manufactured endpoints that the next round of composition can still grow. As long as the bars stay high, the machine is not running out of new mathematics; the campaign stops the day they decay.
Latest discoveries
from the value index over the banked register, refreshed with each wave
| qS29_H1_560 | ∀ (v : Fin (8 : Nat) → Complex) (r : Real) (hr : LT.lt (0 : Real) r) (M : LightLanguage.CPM.MeaningForced.MeaningObject) (α : Type u0) (s : Set α) (f : α → In | crossover: conclusion touches the institute's derivations, parents did not |
| qS29_H1_561 | ∀ (v : Fin (8 : Nat) → Complex) (r : Real) (hr : LT.lt (0 : Real) r) (M : LightLanguage.CPM.MeaningForced.MeaningObject) (α : Sort u0) (f : α → IndisputableMo | crossover: conclusion touches the institute's derivations, parents did not |
| qS29_H1_562 | ∀ (v : Fin (8 : Nat) → Complex) (r : Real) (hr : LT.lt (0 : Real) r) (M : LightLanguage.CPM.MeaningForced.MeaningObject), Iff (Eq (LightLanguage.CPM.Meaning | crossover: conclusion touches the institute's derivations, parents did not |
| qS06_H1_234 | ∀ (a b c : Prop), Not (Or b c) → Iff (Or (Or a b) c) (Or a c) | load-bearing: already parented 64 certified children |
| qS05_H1_907 | ∀ (a c a_1 b : Prop), Iff a (Or a_1 b) → Iff (Or a c) (Or (Or a_1 c) (Or b c)) | load-bearing: already parented 63 certified children |
| qS06_H1_145 | ∀ (α : Sort u0) (P : Prop) (inst : Decidable P) (x y : α) (b : Bool) (x_1 y_1 : α), Iff P (Eq b Bool.true) → Eq x x_1 → Eq y y_1 → Eq (ite P x y) (bif b then | load-bearing: already parented 63 certified children |
What this is
The Recognition Physics Institute built a composition organ over the largest library of certified mathematics in the world plus the institute's own derivations. The organ pairs existing theorems, attempts the compositions mathematicians never wrote down, and keeps only what is new and what the kernel certifies. It then feeds its own output back in as raw material, so each generation of theorems composes the previous one. This page reports that campaign as it runs.
Two kinds of support, stated plainly: every theorem in the count is kernel-certified (the strongest support mathematics has), and the stopping rule is preregistered: the campaign halts and reports if novelty decays, duplication rises, or failures break out of their measured envelope.
Why Stage B changes the question
The engine works by matching the conclusion of one theorem to the hypothesis of another and welding them. When both parents are fully concrete, that saturates: everything reachable is reachable in one step, and more passes add nothing. That was proved and banked. What breaks the saturation, and why the current design works at all, is that welding general statements manufactures new objects that were not in the library, so each generation opens match sites the previous one did not have.
So Stage B will compound. The question is what compounds. A chain of N welds is a longer proof, not a deeper theorem, and length is not what makes mathematics matter. The measured signals say the same thing: about 55 percent of first-generation results get used as an ingredient by a later one, and about 5 percent become heavily reused, and those two numbers are nearly identical whether Recognition Science is in the base or not. That is an engine running at a stable rate, not one accelerating into new territory.
Unknown mathematics can still appear by one route. Every so often, a manufactured object will happen to be something a mathematician would recognize as natural, and then a statement about it is a real theorem rather than plumbing. The chance per item is tiny. The item count is enormous and growing. That is a lottery with a real ticket rate, and the whole question is whether the ticket rate falls faster than the count rises. That is measurable: take a fixed sample from each generation, audit it by the same standard, and record how many survivors per hundred thousand each generation yields. If the third generation matches or beats the first, scale wins outright and Stage B should run to the end. If it collapses to near zero, the machine is compounding glue and the effort belongs on steering what it composes rather than how many times.
Receipts
The institute: recognitionphysics.org
The public certified library: github.com/jonwashburn/recognition-science
Live instrument state: cambrian-wave.json