Technical report

TRINITY, mostly in diagrams.

Our own report on the software behind this site — written to be checked, not believed. Every claim points to something public; the weak parts are marked weak. The code is not published; the output, the reasoning and the papers are.

Status of the instrument

Not finished, and not a success yet.

TRINITY is an instrument that needs tuning — a microscope is only as good as its lenses, and ours are still being ground. The aim is not one clever model but a family of them, each tuned to a different sector. Curious things can already be done with it; that is not the same as having arrived.

This is our own account of our own work, not an outside audit or certification. Written by the developer — not a mathematician by profession, nor a specialist in formal verification or law. Outside official bodies we do nothing in cybersecurity, and nothing in that direction without their guidance (INCIBE first) — see About and Terms.

The object of the report

What it is, and is not

It is

A family of software models for large-scale, exact-arithmetic mathematics. The build behind this site is the generic test model test_min_max_0, honest stage pre-alpha (Methodology, Status).

It is not

Not a trained model, not a chatbot, and it decides nothing about a person. The visuals here are deterministic computation, not AI-generated media (Compliance).

What it can do

Produce candidate results in number theory, combinatorics and exact linear algebra, cross-check them, and hand a subset to a proof assistant. It solved a chess endgame exactly (399,112 positions) and replicated Axelrod’s tournament.

What it cannot do

It has solved no Millennium Prize Problem and does not claim to. A V result is exact within a stated range and silent outside it; more computing does not make an unproven thing true.

The method, in one picture

It reads a problem for a signal — and tunes at the point of tension

The closest analogy is signal detection: TRINITY builds its own models over a problem and tests whether a signal survives controls. A false signal is worse than none — the error compounds and can go catastrophic — so the whole method is built to control that error, not chase the pattern. On Riemann, all three signals came out no pattern: the correct answer, not a failure. This shape was learned on Collatz.

Tuning: press to the point of tension, not the maximum As you press a problem harder, more of its structure is revealed, up to a point of tension just before it snaps. The usable datum falls out there. Press past it and the structure breaks and yields nothing. the datum falls out here point of tension press harder → it snaps structure revealed pressure on the problem →
Tuning is not adding power. It is finding the formula that crushes a problem into a shape you can observe, then pressing — not to the maximum, where it breaks and gives nothing, but to the tension point just before, where the datum falls out. Finding that point, problem by problem, is most of the work still ahead.
Architecture

Engine at one end, what you can read at the other

How TRINITY connects to what you can read Step 1, the engine, which is not published, produces a candidate result. Step 2 is that candidate result. Step 3, the validation pipeline, checks it by independent methods and, where possible, a machine proof. Step 4, only what survives is published, on this site and as deposited papers. When two methods disagree the candidate is sent back to a person to review, fix and re-run. 1 2 3 4 TRINITY engine Candidate result Validation Published not published pipeline (detailed below) site + papers disagreement → a person reviews, fixes, re-runs
Nothing crosses from candidate to published without surviving the pipeline. The dashed arrow is the one that matters: a disagreement is not smoothed over, it is sent back to a person. The code is offered, in full, to regulated public bodies in the UK and Spain on request (About).
Symbolica, adapters, and where it runs

A hexagonal core, and everything else an adapter

Symbolica: a hexagonal core with adapters At the centre is Symbolica, a pure domain of patterns, discoveries and theorems with its use-cases. Everything external is an adapter around it: run locally where it builds its own model, run through an AI over an API where a Claude adapter exists, run on Cloudflare Workers AI through its adapter, a Lean 4 adapter, and a database adapter. Around ninety plugins register through the core and switch on and off independently. Symbolica domain · use-cases Run locally builds its own model API — AI Claude adapter Workers AI over HTTP Lean 4 proof adapter Database a real store ~90 plugins on / off
Underneath the plugins is Symbolica: a pure domain wrapped in adapters, which is exactly what lets the same core run in more than one place and any plugin switch on or off. The local and Claude API adapters exist, and the Cloudflare Workers AI adapter now exists too — it reaches a Workers AI model over HTTP, reading its credentials from the environment (never hard-coded), and it is covered by the same adapter tests as the rest. It runs when those credentials are set, the same way the Lean adapter runs when a Lean toolchain is present. The flight report records which plugins lit and which did not.

On the order of ninety small, self-contained plugins, named by family not by function — what a plugin does is part of the engine that is not published, and naming one is never a claim it works: the Birch–Swinnerton-Dyer block, the Hodge family, the Riemann–Redheffer line, Collatz and accelerated dynamics, combinatorial games (the chess endgame, Althöfer’s prize game, the Wythoff-inspired work), the Clifford / Gottesman–Knill case, the Lean 4 bridge, Conway’s Life and the generative visuals, and the self-audit layer that flags whether a result looks original. Lines that have published nothing are not named here until they do (Methodology).

The flight report

What was launched, what lit, and what came out

The flight report for the build behind everything here — drawn, not only described, because the failures are the content and not the footnotes. The full write-up, engine by engine and problem by problem, is on Status.

36/37

engines lit

132

findings recorded

26

closed by Lean 4’s kernel

18

refutations, kept on purpose

The engines: what was aboard, what lit 91 plugin files in the tree; 37 register through the loader; of those, 36 lit and 1 did not. The one that did not light fails at import, which means it never runs at all - not that it runs badly. 91 plugin files in the tree 37 the loader tries to bring up 36 lit 1 dark (fail at import) Measured 2026-10-05, by starting the system — not read off a list. It exposes 17 tools.
Of 91 plugin files, 37 register through the loader and 36 light. The one that stays dark fails at import, not at run time: a library it needs is not available in the measurement environment, and it is exactly the engine that computes the global side of Birch and Swinnerton-Dyer — so the limit in the machine and the limit in the mathematics are the same limit. Measured by starting the system, not read off a list.
What came out: 132 findings, by level of certainty 26 at P-Lean (Lean 4's kernel accepted it); 10 at P (Proved, written out); 60 at V (Exact in a stated range); 18 at H (A lead, no verdict); 18 at X (Refuted, kept on purpose). Total 132. The X column is refutations, kept on purpose so the same dead end is not walked twice. 26P-LeanLean 4's kernel accepted it10PProved, written out60VExact in a stated range18HA lead, no verdict18XRefuted, kept on purpose
132 findings, by the level of certainty each carries. 18 of them are refutations (the X column), kept on purpose so the same dead end is not walked twice — a record that only ever confirms itself is checking nothing. Only the 26 at P-Lean carry the strongest claim: closed by Lean 4’s kernel. Every finding is on Challenges with its exact range and, where it exists, its refutation.
Validation — and where a human sits in the cycle

A person is in this loop at more than one layer, not just the entrance

Two things are true at once: an AI coding agent is genuinely in the loop, and no result is trusted because a model produced it. The marked layers below are where a human actually sits — the input, the build, the tuning, and every disagreement — not only the way in.

The validation loop, and the human layers in it A cycle of seven stages. A human states a hypothesis, possible theorem or axiom; a human developer and an AI coding agent build the code together; a human tunes where to press. The result is then computed by two independent methods, cross-checked, closed by the Lean 4 kernel where possible, and published with its level. A human sits at four of these layers, marked: the input, the build, the tuning, and the review of any disagreement, which loops back to the build. It is not only the entrance. disagree → a person reviews, fixes, re-runs the loop Input a hypothesis, theorem or axiom Build human developer + AI coding agent Tune press at the point of tension Compute two independent methods Cross-check agree / disagree Prove Lean 4 kernel, where possible Publish with its level: P-Lean / P / V / H / X where a human can sit — the input, the build, the tuning, and every disagreement
The marked layers are the human ones. It is built to keep growing more of them — more layers, custom stages — which is the scaling and professionalisation still ahead, and why the diagram is a cycle rather than a two-step demo. The live example of the two-method cross-check is the Redheffer chart: a matrix determinant checked against an independent Möbius sieve.

The AI agent, plainly

Parts of the code are built with an AI coding assistant (Claude, Anthropic) — disclosed, not hidden (Compliance). It helps write and check code; it decides nothing true and never talks to visitors.

Lean 4, honestly

26 findings are closed by the Lean 4 kernel (P-Lean, the strongest guarantee here). Where a theorem is closed by native_decide it trusts the compiler, not the kernel, and is not called kernel-checked. The KRK paper was corrected for exactly that.

The site checks itself

A full battery of automated checks runs before every deploy, and the number that fail is shown in the seal at the foot of every page, not asserted. Integrity is recomputable on Provenance.

Every claim wears its level

P-Lean kernel-accepted · P proved, written out · V exact in a stated range, silent outside · H a lead · X tried, false, kept. The key is on Methodology.

The quantum work

Exact only where it can be, on real hardware

General quantum simulation cannot be exact the way the rest of this work means the word — one Hadamard already gives a rounded number, and we do not claim otherwise. What is exact is the Clifford / stabilizer case: by the Gottesman–Knill theorem such a circuit is a binary matrix, computable with no floating point — deposited as a paper (Exact Entanglement Entropy and Code Distance for Stabilizer States) and checked against Qiskit across 15,800 random circuits with zero exceptions. The relevant runs executed on IBM Quantum’s real processors, job identifiers recorded — and that hardware is never launched autonomously: a run happens only on an explicit human decision.

The record

What it was put to — failures kept on purpose

Four Millennium Prize Problems

Hodge, Birch–Swinnerton-Dyer, Riemann, P vs NP. Not solved, not claimed. The method is to chip: prove a small piece, machine-check where possible, keep the false attempts (Challenges).

Collatz, where the lab began

The reason most of the exact-arithmetic tooling exists. One proven piece is stated with its exact congruence on Challenges; you can hear its 2-adic valuations as notes, live.

Solved, exactly

King + Rook vs King: all 399,112 positions by retrograde analysis, max distance-to-mate 32 matching the classical bound (solved here). Axelrod re-run from scratch; Goldbach and Legendre checks.

Refutations, kept

A large share of the record is refutations — dead ends kept so nobody walks them twice. A system that only ever confirms itself is checking nothing.

How to check this, and one request

Nothing here asks to be taken on trust

Every claim resolves to something public: deposited papers with DOIs (Publications), findings with their levels and refutations (Challenges), cross-checks that run in your own browser (The Notebook), the recomputable integrity manifest (Provenance), and the test count in every page’s footer seal. The code is not published — but it is offered, in full, to regulated public bodies in the UK and Spain on request, at oficial@kodamaseclabs.com.

One request. Working alone and mostly outside the academic circuit, it is easy to rediscover a known result or build on someone’s idea without knowing whose it was. We are actively looking for the references we are missing — prior work our findings may duplicate, and the proper credit for what inspired them. If you recognise a result or know the citation, please say so: the attribution note and how to reach us are on Challenges. Naming the author, and where an idea came from, matters here.