Cambrian / Non-LLM AI for discovery
A deduction in use / 17–18 September 2026
An infinity of histories.
A bounded result.
A calculation can contain infinitely many terms and still fail to define a usable result. For the specified source–photon construction, the research had to establish that the full history sum exists and does not cancel to zero. Cambrian supplied a connecting theorem in that proof.
The result
‖Kψ‖ ≤ A ex ‖ψ‖
All chronological orders. The complete native photon space. No particle or mode cutoff.
Bounded. The full sum has a finite, explicit bound.
Nonzero. At least one normalized coherent state has a nonzero matrix element: the histories do not all cancel.
Reusable. The result supports further proofs about energy and joint source–photon evolution.
- 01 / The question
Does the full calculation mean anything?
The calculation sums source–photon interactions over arbitrarily long ordered histories. The question is whether those terms produce a bounded, nonzero operator on the full photon space.
- 02 / Cambrian’s deduction
A witness that survives cancellation.
Given two proved parent results, the non-LLM engine generated the theorem connecting chronological-history regularity to a nonzero Gaussian Fourier witness. Lean checked the emitted proof.
- 03 / The complete operator
Every state. Every order.
Research agents carried that witness into the full photon space, constructed the bounded operator K, and proved that its original ordered series converges to exactly that operator.
- 04 / The next discovery
A foundation for further physics.
Follow-on proofs preserve the free-energy operator domain and establish unitary joint evolution for the specified adjoint-paired construction. Each result uses the preceding mathematics.
A generated theorem becomes part of a larger proof. The connecting result helps establish a complete infinite-dimensional operator. Further proofs then use that operator to study energy and joint evolution.
The exact statement, assumptions and attribution
The original history operator is Kψ = ∫ c(h) W(β(h))ψ dμ(h). Its chronological terms satisfy ‖Km‖ ≤ A xm/m! and sum in operator norm to K, where A = ‖ξ‖ ‖η‖ and x = T |ℏ|−1 ∑ℓ ‖Mℓ‖.
The construction assumes finitely many bounded source couplings, a supplied strongly continuous source-isometry family with strongly continuous inverse, nonorthogonal source vectors, nonzero photon profiles, positive CE, nonzero ℏ and T ≥ 0. Nonzero means that some coherent-state matrix element is nonzero; it is not a uniform lower bound on every state.
Cambrian generated the connecting witness theorem from selected, supplied parents. AI research agents authored the analytic prerequisites, operator construction and subsequent extensions. Saved Lean builds and axiom audits verify these mathematical results. Selecting the physical interaction and identifying this construction with its physical propagator remain further research; this result does not determine the fine-structure constant.
The native Cambrian engine
Discovery through
mathematical structure.
Cambrian reads theorem statements as structured mathematical objects. Its native engine matches compatible results and constructs a consequence with a proof term. This composition process runs without a language model.
- 01 / Read
Start from proved knowledge.
Read theorem statements, their types and their assumptions as structured mathematics.
- 02 / Discover
Find a new consequence.
Match compatible results and construct a conclusion, checking its statement against the supplied library.
- 03 / Prove
Produce a checkable proof.
Build the proof term and submit it to Lean. Keep the result when the mathematical checks pass.
- 04 / Reuse
Build the next argument.
A generated theorem can become a parent of another deduction or a step in a larger scientific proof.
Each example identifies the engine’s contribution and the surrounding work by researchers and external AI proof authors. Newness is checked within the supplied formal library; historical priority requires a separate literature review.
New discoveries / September 2026
Energy, evolution
and spatial response.
The photon-history construction supports further proofs of energy control and unitary evolution. A separate Cambrian composition gives an estimate for spatial response.
The complete history preserves the energy domainPhoton mathematics · An infinite sum with controlled energy action
Lean-verified supporting analysis · Builds on Cambrian’s generated witness
The original history operator maps every vector in the maximal domain of the native free-energy operator back into that domain. Its energy action is exactly the integral of the proved displaced-energy expression.
The proof retains all histories and the complete photon space. It adds no particle or mode cutoff and no assumed domain-preservation premise. The domain here is the energy-operator domain, which is a stronger condition than merely having finite mean energy.
AI research agents authored this extension of the existing Cambrian-supported construction. The source, saved build and 42 standard-axiom audit results are identified in the evidence summary.
From a bounded history to unitary joint evolutionSource–photon mathematics · The signed adjoint-paired construction
Lean-verified supporting analysis · Exact source compression
Pair each source coupling with its adjoint and each photon profile with its negative. Under the stated original data and complete source-space assumptions, the resulting joint source–photon history is a surjective linear isometry: a unitary evolution.
Its source compression is exactly the original photon-history operator, with the sharper bound ‖Kψ‖ ≤ ‖ξ‖ ‖η‖ ‖ψ‖. The construction keeps the full photon space and allows infinite-dimensional source spaces.
Research agents proved this signed construction in the Cambrian-supported chain. The source couplings and evolution remain supplied inputs; this theorem does not select the physical interaction. Evidence and scope ↗
One response estimate, even as the spatial grid growsNative Cambrian composition · A finite-lattice bound and soft-mode limit
Native engine emission + checked application · Direct Lean and Lake verification
The exact finite Fourier identity connects translated square-current responses on a periodic cubic grid to transverse Fourier modes. For a real field supported on positive lattice symbols λ ≤ ε, the response Q and transverse norm squared E obey:
0 ≤ A E − Q ≤ A ε E / 8
Here A = aE/CE², with aE ≥ 0 and CE > 0. When E = 1 and ε tends to zero, Q tends to A even when grid size varies. If aE > 0 and ε ≤ 4, Q is strictly positive. The zero-symbol response remains zero and is excluded from the occupied transverse support.
Cambrian composed the supplied spatial identity with the supplied estimate. The unchanged engine emitted one theorem; four controls rejected unrelated premises, an insufficient bound and a duplicate. The emitted proof and its downstream application passed both direct Lean checks and a targeted Lake build.
This proves the estimate for fields meeting the stated support and normalization conditions. Constructing the physical field sequence, selecting a vacuum and deriving a physical coupling remain subsequent work. Evidence and verification hashes ↗
Earlier discoveries / The wider research program
Five problems.
Five checked results.
External AI proof authors working within the Cambrian program closed these gaps in the institute’s research library. They range from a grid-independent bound to exact characterizations and infinite families. Open each result to see the problem, the proof and the assumptions it requires.
One stability bound, every grid resolutionMathematical analysis · A guarantee that survives refinement
Lean checked 16 Sep 2026 · Third-party AI author; model not recorded
On the specified cubic grid, the weighted absolute row mass of the discrete Dirichlet Green kernel is at most R2/8, where R is the side length. The same bound works at every mesh level.
The exact bound. For R > 0 and every integer L ≥ 1, take L points per axis and spacing h = R/(L + 1). Let A be the cubic Dirichlet Laplacian, with diagonal 6/h², nearest-neighbor entries −1/h² and zero boundary values. If AG = I/h³, then for every grid point x:
∑y |G(x,y)| h³ ≤ R²/8.
The factor h³ is the volume weight per grid cell. This is the estimate that stays fixed as L grows.
The proof establishes one constant before choosing the grid resolution, so the bound applies across all refinements.
Researchers can refine the calculation without this estimate deteriorating. Uniform estimates are a key ingredient in connecting discrete calculations to continuous mathematics.
This is a proved bound for the stated finite Dirichlet problem. It does not by itself prove convergence of an entire physics simulation.
Formal results: green_row_mass_uniform_bound gives a bound uniform in grid resolution; green_row_mass_le_Rsq_div_eight supplies the explicit R²/8 estimate.
Six edge changes. One invisible direction.Geometry · Exactly which change preserves the angles to first order
Lean checked 16 Sep 2026 · Third-party AI author; model not recorded
At the studied reference tetrahedron, every change of squared edge lengths that leaves the dihedral angles unchanged to first order is a uniform scaling. The angle Jacobian has a one-dimensional kernel, or equivalently rank five.
A researcher working with this discrete geometry can distinguish a change of overall size from a change of shape. The result removes uncertainty about the exact degeneracy of the local geometric calculation.
The calculation concerns the specified reference tetrahedron and its linearized angle map.
Formal result: flatAngleJacobian_kernel_span
An exact condition for rotating quantum measurementsQuantum mathematics · Necessary and sufficient conditions
Lean checked 16 Sep 2026 · Kimi-family AI author
For two real symmetric matrices that each square to the identity, every unit-circle combination also squares to the identity if and only if the matrices anticommute.
These matrices represent an important class of two-outcome quantum measurements. The result identifies precisely which pairs support the full rotation family.
The characterization applies to the stated real symmetric matrix model, at every matrix size.
Formal result: symm_invol_rotate_iff_anticomm
One agreement point, across every natural-number dimensionInstitute model · A uniqueness theorem over all natural numbers
Lean checked 16 Sep 2026 · GPT-family AI author
Across all natural-number dimensions, two dimension-dependent exponent formulas in the institute’s model agree if and only if the dimension is three.
A universal theorem closes a logical gap that checking additional examples cannot close.
This establishes uniqueness within the specified formulas. Their physical interpretation is a separate research question.
Formal result: k_fib_eq_k_int_iff_dim_three
An exact Fibonacci formula for an infinite familyNumber theory · A Fibonacci expression valid at every positive even exponent
Lean checked 16 Sep 2026 · Third-party AI author; model not recorded
The institute’s cost function, evaluated at every positive even power of the golden ratio, has an exact expression in neighboring Fibonacci numbers.
Researchers get an exact general expression to use in later mathematics, with no need to establish each case separately.
The result applies established golden-ratio and Fibonacci identities to the institute’s cost function.
Formal result: jcost_phi_pow_even_eq_fib
Dates identify the recorded library landings. On 16 September 2026, the institute rebuilt the five theorem sources and all 95 project dependency modules, then audited the five featured theorems and the explicit R²/8 Green-bound result using only standard mathematical axioms. Read the public evidence summary.
A discovery, step by step / Quantum mathematics
Discover what
examples cannot prove.
The Cambrian research program took a calculation for particular quantum-measurement matrices to a general theorem and its converse. Here is the recorded path within the research library.
- 01 / The general question
Two matrices worked.
What about every size?The library verified particular two-by-two quantum-measurement matrices entry by entry. Cambrian’s research tools identified the missing general statement.
- 02 / The discovery
A theorem for
every matrix size.The research identified sufficient conditions for an entire family of measurement rotations. An external AI prover supplied the proof; Lean checked it.
- 03 / The next result
Then prove the
condition is necessary.A later AI-written proof established the converse. The final equivalence combines that new necessity proof with the earlier sufficiency theorem.
- 04 / The research use
A general result
the research can reuse.The first theorem replaced the special-case step in a proof attaining the quantum correlation bound. The later result characterizes exactly which matrix pairs allow those rotations.
Recorded 11–12 August 2026. A generalization and its converse within the institute’s library; the physical interpretation is the stated mathematical model. Read the theorem and attribution ↓
From the verified source
Written in Lean.
Exact Lean excerpts from the AI-authored results. These final steps connect supporting lemmas into the quantum characterization and geometry theorem. The in-house generator’s complete proof body appears below.
Quantum mathematics
Two directions. One equivalence.
Final assembly: one supporting lemma proves necessity; the earlier theorem supplies sufficiency.
constructor
· intro hrot
exact anticomm_of_symm_invol_rotate M N hMsym hNsym hMinv hNinv hrot
· intro hanti c s hcs
exact (symm_invol_rotate M N hanti hNinv hMinv hNsym hMsym hcs).2Geometry
The exact geometric freedom.
The final declaration states the geometric freedom. The invoked lemmas establish the kernel calculation.
theorem flatAngleJacobian_kernel_span (v : Fin 6 → ℝ)
(hv : ∀ f : Fin 6, ∑ g : Fin 6, flatAngleJacobian f g * v g = 0) :
∃ c : ℝ, v = fun g => c * freudenthalTetSqEdges g :=
rawJacobianCoefficient_kernel_span v ((kernel_flat_iff_kernel_raw v).mp hv)These excerpts rely on supporting lemmas; they are not standalone proofs. Scroll within a code panel to read long lines. Complete sources and dependencies remain available through an agreed review.
Within the institute’s research
What the proofs
make possible.
Cambrian’s in-house generator constructs new theorem statements together with their proofs, filters out duplicate statements in its supplied library, and can use a generated result in a further deduction. In these examples, AI research agents supplied the surrounding mathematics; generated lemmas became checked steps in larger research arguments.
The in-house generator / Fundamental physics
A checked step the next argument can use.
The Cambrian generator wrote this proof connecting two existing lemmas. Under their stated assumptions, the result preserves an inner product. The surrounding lemmas were supplied by other AI research agents; the generated result is then used in the quantum argument below.
Its value is what depends on it: the generated theorem is invoked in the larger checked argument. Authorship of the surrounding mathematics remains with the research agents.
by
intro x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
exact Eq.trans (@CambrianLoadedUnital.reverse_loaded_to_paths.{u0} x0 x1 x2 x3 x4 x5 x6) (@CambrianLoadedUnital.reverse_paths_to_input.{u0} x0 x1 x2 x3 x4 x7 x8 x9 x5 x6)An infinite calculation. A finite error bound.Quantum mathematics · Generated theorem used in a convergence proof
Native Cambrian theorem · Saved Lean verification, 16 Sep 2026
If a quantum calculation contains infinitely many terms, controlling each term separately does not automatically control their total error. What conditions make the full approximation reliable?
Under a stated bound on coefficient sizes and a uniform bound on approximation errors, the full series of integral errors converges and its total has an explicit finite bound. As the uniform approximation error tends to zero, the total error tends to zero too.
The native generator produced a theorem connecting a supplied infinite-series certificate to a supplied general error estimate. The surrounding research proof calls that generated theorem directly, with its emitted source unchanged.
The combined proof controls the complete infinite sum, without imposing a finite cutoff. A checked counterexample also shows why convergence term by term would be insufficient.
One generated theorem passed, and four deliberate rejection checks passed, including a repeated-statement check. The run tests the stated theorem and rejection controls; it does not measure a success rate across research problems.
Saved verification records cover five final targets, including the generated source, actual integral application and counterexample. Other AI research agents supplied the scientific setup, parent proofs and application. Together, these checks establish the specified mathematical approximation step.
A checked premise for the next quantum-physics argumentMathematics for physics · Used in internal AI analysis
A formal research package proves that the modeled quantum transformation preserves the identity operator under explicit reversibility and model assumptions. It also provides a checked counterexample to weaker assumptions.
The displayed generated lemma, CambrianLoadedUnitalGenerated.reverse_inner, joins two existing equalities to preserve an inner product under the supplied assumptions. It is used in the final argument. The fifteen-module package includes that contribution and the surrounding mathematics and counterexample developed by other AI research agents.
An internal AI agent working on physics inspected the sources and saved verification records, then used the result as a premise in further stationary-state analysis. It did not perform a fresh proof-checker build.
The saved verification covers the fifteen-module combined argument. The later analysis is a separate contribution; neither a stationary physical state nor a new experimental prediction is established by this theorem alone.
A proved error bound for an atomic-physics calculationAtomic-physics mathematics · Selected by an internal AI agent
Under the stated stability and boundary conditions, the error in the specified polynomial calculation is bounded by the sum of its local equation defects.
The in-house generator produced CambrianClenshawGenerated.clenshaw_full_defect_bound: one theorem joining an existing exact error identity to an existing norm bound. Under the supplied stability and zero-endpoint assumptions, the polynomial calculation’s total error is at most the sum of its local equation errors. The final application uses it to control calculation error; the surrounding argument was developed by AI research agents.
An internal AI agent working on atomic physics inspected the proof and verification records, then selected the package for its next calculation.
The record establishes selection by that internal AI agent. It does not establish a completed numerical calculation using the result or a new atomic-energy prediction.
Proof & evidence
A theorem carries
its proof.
It states what is true, under which assumptions, and supplies a proof that a separate checker can verify.
Lean checks the mathematical deductions. The five theorem entries were freshly checked in Lean on 16 September 2026. Their verification records pin the source files and compiled outputs; the later research-use entries identify their own saved checks. A correct proof can then become a dependable premise for the next piece of research.
What is new about these theorems?
These proofs resolve specific questions in the institute’s research library: a bound uniform over every grid, a missing converse, an unrestricted dimension result and an exact infinite family.
The record establishes what each proof adds to that library. Priority across the mathematical literature requires a separate literature review.
What did Cambrian do?
Cambrian itself is a non-LLM discovery engine that constructs formal statements and proof terms. The wider research program brings that engine together with human direction, AI research assistants and independently checked proofs. In the August research workflow, third-party AI agents wrote the featured proofs. The recorded proof authors include a GPT-family agent for the dimension result, and a Kimi-family agent for the quantum converse. In the September examples, the in-house generator supplied connecting proofs within larger AI-developed arguments.
Jonathan Washburn directs the research. Lean checks the proofs. The record does not establish autonomous research without that surrounding work, or superiority over frontier AI on a matched benchmark. Cambrian’s proprietary methods remain private.
Does Cambrian discover science, too?
Cambrian supports scientific discovery by producing mathematical deductions that further research can use. The wider research team develops the theoretical arguments and physical identifications. In the work behind The Four Indices, it characterized which coordinate descriptions fully represent the institute’s geometry, and explained why an extra coordinate would be redundant. The research identified an insufficient assumption and supplied the stronger characterization.
That is theoretical discovery within the stated mathematical model. It came from the human-directed research workflow using AI agents. The specialized Cambrian proof generator has a narrower demonstrated role: producing checked steps within larger arguments. These are distinct contributions to the same scientific purpose.
The research ledger records a successful Lean build and axiom audit for The Four Indices on 6 September 2026. That example is separate from the five theorem sources rebuilt on 16 September.
Can I inspect the evidence?
The public evidence summary lists theorem identifiers, scope and verification-record hashes. Selected source excerpts are shown above. The complete sources and dependencies remain private. The hashes identify the records reviewed; they are not complete proof downloads.
Contact Jonathan about a theorem review to discuss source access and confidentiality. Anyone given the complete sources and formal dependencies can check the mathematical claims independently.
How much work does Cambrian save?
The page reports selected completed results. Archived development logs include failed attempts and duplicate proposals, but they do not provide a complete, consistently timed record of attempts, cost and human intervention across the five theorems.
The next proposed evaluation compares Cambrian with the same third-party models run without its in-house generator, on a frozen set of new problems. It would report every attempt, checked completion, time, cost and human intervention. An efficiency advantage remains to be measured.
Does a checked theorem validate a physical theory?
It verifies the conclusion from the stated definitions and assumptions. Whether those assumptions model nature, and whether a calculation agrees with experiment, require their own evidence. Each theorem above states its mathematical scope.
The ambition
Research that
builds on itself.
Every solved theorem can become the starting point for the next discovery.
We are building Cambrian for mathematicians and scientific researchers who need more than a plausible answer. The aim is to make mathematical discovery cumulative: identify a missing general result, establish it, and give the next researcher a stronger place to begin.
- 01
Find the missing general rule.
Recognize where specific examples conceal a general question. Establish the missing implication, the converse, or the universal result.
- 02
Carry the proof forward.
Pass checked results to the next research argument, with their assumptions intact.
- 03
Broaden the test.
Evaluate a frozen set of new problems. Record every attempt, checked completion, time, cost and human intervention; compare against the same third-party models without the in-house generator.
We propose a comparison report that includes failures and receives review from an outside researcher. It should establish whether the generator adds checked completions or reduces total effort, giving us a basis for deciding how to develop it. No outside reviewer or date is committed.
Explore the theorem recordThe people behind Cambrian
Built at an
independent institute.
Jonathan Washburn
Founder and Lead Scientist
Recognition Physics Institute · Austin, Texas
Jonathan directs Cambrian within the institute’s wider research program in fundamental physics and its applications.
Meet the institute’s people · Read the research
Interested in a theorem, a research problem, or the technology? Get in touch.
hello@recognitionphysics.org