Building software for mathematics · calibrating, needs peer review · pre-alpha

Software trying to do mathematics. We publish the working, not just the answer.

Behind this site is a piece of software, and it is pre-alpha. It fails runs, contradicts itself in places, and says so in its own logs and its own flight report. What it will not do is show you a pattern that is not there.

7preprints deposited with DOIs. None peer-reviewed — a deposit is a dated record, not a second opinion 399,112chess positions solved exactly and machine-checked in Lean 4 17exhibits that compute live in your tab, across five rooms 5Lean proofs submitted to Mathlib, the community library. A submission is not an acceptance; where each stands is live
The caveats in full — what fails, what is refuted, and why caution is the method

Not a product, not a service, and not stable in any sense worth the word: one of the engines it loads fails on every single run, one module contradicts a reference table at n=210n = 210 and carries do not use yet in its own docstring, written by us, and the whole of it needs a great deal more refining than it has had. The flight report says exactly how much, engine by engine and problem by problem.

Of 132 recorded findings, 18 are refutations — kept so nobody walks down those roads again, including us. On the Riemann side, all three observables we built come out no pattern, and that is the correct answer rather than a failure. 26 results carry Lean 4’s kernel; the rest are weaker and each says which. A beautiful relation that is not real is worth less than nothing here, because someone would build on it.

The engine is ours and is not published; the results are open. Everything you see moving on this page is computed rather than decorated — the descent behind it is a real logarithmic ruler, and the exhibits run in your browser while you read them. Caution is the method rather than a disclaimer at the bottom: when a proof leans on a compiler instead of a proof kernel we say so and name the axioms, and when a claim is a computation rather than a theorem it is labelled a computation. That is the part we would keep if we had to drop everything else.

Our research programme

What we are actually trying to find out

Three strands, worked on at once because they keep handing each other tools.

Behind this section: the Collatz trajectory of every number up to 2,400, walked backwards from 1 — each even number turns the path one way, each odd number the other — so numbers whose trajectories end alike share a branch.

Strand 01 · 106 findings

Four of the seven Millennium Prize Problems

The Clay Institute’s seven are the most famous open questions in mathematics. We work on four of them: the Hodge conjecture, Birch–Swinnerton-Dyer, the Riemann hypothesis, and P vs NP. We are not solving them and we do not claim to be. We chip: prove a small piece exactly, have a machine check it where that is possible, and write down the attempts that turned out false so nobody spends a week rediscovering them.

Every finding, refutations included →
Strand 02 · 14 findings

Collatz — the one this lab grew up around

Take any number. Halve it if it is even, triple it and add one if it is odd. Everyone believes you always land on 1 eventually; nobody has been able to prove it. It is not a Millennium problem. It is simply where this lab started, and most of our exact-arithmetic tooling exists because of it.

Watch it run →
Strand 03 · 12 findings

Misc research — whatever answers to no single field

Finished results that belong to no one discipline, plus replications we run to check other people’s work instead of taking it on trust. A chess endgame solved exactly, all 399,112 positions of it. Axelrod’s cooperation tournament re-run from scratch. Goldbach and Legendre checks.

Open the Annex →

How to read anything we publish

Every result here carries a label saying how strongly it is known, and that label is part of the claim rather than a disclaimer bolted on afterwards.

  • P-LeanA proof assistant’s kernel accepted it. As sure as anything here gets.
  • PProved, with the proof written out for you to read.
  • VComputed exactly, zero exceptions inside a range we state — and silent about everything outside it.
  • HA lead we are following. No verdict yet.
  • XWe tried it, it was false. Kept so the next person does not lose the same week we did.

If that reads like a lot of caution, it is deliberate. Labelling the weak results honestly is what gives the strong ones any weight — and mostly it keeps us from believing our own drafts.

Research

What we work on

The faint dots moving behind these cards are our own Game of Life rule, B37/S2378, found by searching all 262,144 life-like rules — the same rule at full strength in the museum. Nothing on this page moves unless it is computed.

FIG. 01

Numerical & Mathematical Algorithms

We design advanced algorithms to solve large-scale mathematical and numerical problems, from optimization to computational modeling — with outcomes measured in stronger security guarantees, lower energy consumption, and better runtime efficiency, not benchmarks alone. Key results are formally verified using the Lean theorem prover and its Mathlib library, rather than relying on manual proof alone — see exactly which ones, and how, on Methodology.

Smith's determinant, live. The grid is the matrix of gcd(i,j), darker where the gcd is larger. Its determinant equals φ(1)·φ(2)⋯φ(n) — Euler's totients multiplied out — because the matrix factors as Zᵀ·D·Z through the divisibility lattice. Both sides are computed exactly here, every step, in integer arithmetic; we formalised the theorem for Mathlib (how).
FIG. 02

Interpretable Machine Learning

We develop machine learning models that are efficient, sustainable, and transparent — systems whose decision-making process can be audited and understood.

The judge's bar moves. Each dot is a candidate detection at height p·IoU. It is taken (filled) exactly when that exceeds half the current panoptic score — the staircase — because adding a candidate grows the score's denominator by one half whether it matches or not. So the bar rises as the judged set improves, and a dot that would have passed early is refused later. Proved in Lean (how); greedy, not globally optimal, and it says so.
FIG. 03

Post-Quantum & Quantum-Inspired Computing

We monitor and evaluate cryptographic schemes designed to remain secure against quantum computers, and study quantum-inspired algorithms — techniques drawn from quantum computing that run efficiently on conventional hardware. What that actually looks like today, concretely, is on Methodology.

The same mathematics, small enough to watch. A Kyber-style cipher in Z42[x]/(x8+1): one byte per message, public key (A, A·s+e), ciphertext (A·r+e1, t·r+e2+m·q/2). Decrypting leaves each bit plus a noise term e·r−s·e1+e2 — the bars — and the bit survives exactly when the noise stays inside ±q/4, the shaded corridor. At this toy size it sometimes doesn't (red), which is the point: Kyber's real parameters keep the same corridor and make that probability 2−139. Computed live on a seeded stream; the identity, the corridor rule and the failure rate are recomputed in the build.
Why it matters

The world quantum computing is walking into

Quantum computing isn't just faster hardware — it's a different model of computation, and parts of it are already forcing decisions today, not someday. No hype, same rule as everywhere else on this site: four things worth knowing, plainly stated. The mathematics behind the first one runs, on a number small enough to watch, in the descent.

01

The security clock is already running

Shor's algorithm, run on a sufficiently large fault-tolerant quantum computer, would break the RSA and ECC encryption most of the internet still relies on. That computer doesn't exist yet — but "harvest now, decrypt later" means encrypted traffic intercepted today can simply be stored and broken once it does. Data with a long shelf life is exposed by that gap regardless of when the hardware actually arrives.

02

We're in the noisy middle

Today's devices are what the field calls NISQ — Noisy Intermediate-Scale Quantum: tens to low thousands of qubits, without full error correction yet. Real research runs on them, ours included (see The Notebook for actual IBM Quantum hardware runs, logged live). But a durable, useful quantum advantage on real-world problems is still the frontier, not the baseline — steady error-correction progress narrows that gap, it hasn't closed it.

What noisy actually looks like, measured. Our own GHZ(n) circuits on ibm_kingston (4096 shots each, job identifiers in The Notebook): an exact circuit would return only 0n and 1n, and the hardware's fraction on those two strings falls from 94.4% at n = 3 to 88.3% at n = 7 — the ladder on the left, a division per rung. On the right one run is replayed from its recorded counts, shot by shot, with the 95% interval of the running estimate closing in on the full run's value: a hundred shots cannot tell the rungs apart, four thousand can. Recomputed from the published counts in the build.
03

The practical response already exists

You don't need a quantum computer to defend against one: NIST-standardized post-quantum algorithms such as Kyber and Dilithium already run on today's ordinary hardware. The real work is inventory — knowing which systems still depend on RSA/ECC — and migration, not waiting for quantum computers to arrive before reacting. A Kyber-style cipher small enough to watch runs under What we work on, above; our own inventory of what actually runs where is on Methodology, not just claimed here.

04

Where we actually fit in

KodamaSEC doesn't build quantum hardware. We monitor post-quantum cryptographic standards as they mature, and study the quantum-inspired algorithms described further up — the ones that run on the hardware everyone already has. That's a deliberately smaller claim than "we do quantum computing" — and it's the one that's actually true today.

What we do

We research, we publish, and we build software — without lying about any of it

Three things, and one rule over all of them: nothing here claims more than it rests on. A result says how strongly it is known, a refutation stays in the record, and a draft is never dressed up as a finding.

Research · 132 findings

We research

Exact computation and machine-checked proof on open questions in mathematics. Every finding goes into a public registry with its level of evidence — 26 accepted by Lean 4’s kernel, and 18 refutations kept on purpose, so nobody walks down those roads again.

The registry, refutations included →
Publish · 7 preprints

We publish

Seven preprints with DOIs and four records in the Lax Lean Archive, rebuilt by the archive’s own Lean kernel before it accepted them. None of the preprints has been peer-reviewed yet; a DOI dates a result, it does not vouch for it.

Everything published →
Software · 17 live exhibits

We build software

The code behind each result, and the instruments on this site: seventeen exhibits and three tools that compute in your tab, in exact arithmetic, showing the steps. The research engine itself is ours and not published; what it produces, and the software around it, is.

Use the tools →

Open source, and contributing

The separate company once planned in Tenerife will not be set up. KodamaSEC carries on as open source: the code, data and proofs behind each result go into public repositories, and the proofs good enough for other people’s projects go to them — five pull requests to Mathlib, the Lean community’s library, each with its state live. A submission is not an acceptance, and the page says which is which.

To be direct about what we are not: KodamaSEC will not sell cybersecurity products, services, consultancy, audits, training or studies, and will not enter any commercial relationship connected to cybersecurity — now or later. The reasoning is on About. What we do instead is publish, free to read and free to disagree with. For anything else, see Contact.

Where the mathematics runs

Not slides. Live mathematics, computed in your tab.

Three places on this site compute rather than describe. Each one says what it rests on.

01

The Descent

The former front page, kept whole: a fall through 47 orders of magnitude, from the observable universe to the floor of measurement, with one exact physics per scale, a sea of Gerstner trains, Shor’s period-finding on a number small enough to watch, and seven exhibits that compute as you scroll. Long on purpose; this page is not.
02

The Notebook

Seventeen exhibits across five rooms: Lean-verified theorems, IBM Quantum hardware runs logged live, the Collatz map stepped exactly with BigInt, the solved chess endgame. Each entry states what it rests on.
03

Tools

Three instruments rather than demonstrations: you type your own number in and they answer about your number, in exact arithmetic, showing the intermediate steps — including the ones that make an answer inconvenient. Nothing is sent anywhere.