Moving visuals on this page — measured at 0.26% brightness change per frame and zero flashes per second; your reduce motion setting stops them. What moves, and how it was measured
Mathematical plates that draw themselves — prime counts, orbits and lattices rendered live rather than shipped as pictures. It runs continuously while on screen, and it pauses on its own whenever it scrolls out of view.
We measured it rather than guessing: the largest frame-to-frame change in average brightness is 0.26%, and it produces zero flashes per second against the threshold of three set by WCAG 2.3.1. That is well under the limit, and it is not a promise about any individual: if moving images are a problem for you, you should not have to assess ours.
Everything animated on this site honours your system’s reduce motion setting — turn it on in your operating system or browser and these pages stop moving, with nothing else lost. All the mathematics is in the text and the still figures.
14 pieces of working mathematics, each one running as you read it.
Most entries compute in your browser as you read; the rest say plainly what they are — recorded hardware data, or an argument. It is filed under 5 categories — pick one in the bar above, or start with any entry below; each one carries two labels: what you can do with it, and what it rests on.
Research status: this is KodamaSEC’s own in-progress research and none of it has been peer-reviewed. Machine-checked is a real and strong property; it is not the same as reviewed by other people.
Everything, by category
What the two labels on each entry mean
The second label is the point. “Proved”, “machine-checked”, “measured” and “illustrative” are not decorations: they are genuinely different kinds of claim, and most of the mistakes worth avoiding come from reading one as another.
What you can do
- Play with it 5
- you drive it; it responds
- Run it 6
- press it and watch it compute
- Verify it 1
- check our number against your own
- Read it 2
- an argument, not a demo
What it rests on
- Proved 1
- a theorem, not a sample
- Machine-checked 1
- accepted by Lean 4’s kernel
- Exhaustive 2
- every case computed, and an independent implementation agreed
- Measured 5
- computed over a stated range
- Replicated 1
- someone else's result, re-run here
- Argument 1
- reasoning, offered as reasoning
- Illustrative 3
- shown because it is worth seeing
Numbers & structure 7 entries
Structure and complexity: orbits that may never end, primes proved prime, a determinant that agrees with a function it has no business agreeing with, and entangled states measured on hardware rather than simulated.
Sound 1 entry
Pitch is not decorative here: it is chosen by the numbers the exhibits next door are computing.
Knowing 1 entry
Where the mathematics stops and the epistemology starts. What a proof buys you, what a computation buys you, and why those are not the same purchase.
Machines 2 entries
Digit by digit, where the abstraction leaks: exact arithmetic against floating point, integrators that drift, and the physical scale of the numbers involved.
Curiosities 3 entries
Every museum has this room, and most of them call it something apologetic. These are results that are real and finished and simply do not belong to one subject — a solved game is not philosophy because it raises a question, and not number theory because it counts things. They are here because they are worth looking at, not because they were left over.
The Factory not an entry
The same mathematics as the entries above — the Mertens function computed exactly, a Game of Life growing on top of it — but it takes the whole page and is meant to be watched rather than read, so it has no category and no evidence chip. If you want one thing from here that is pleasant to leave open, it is that one. Open the Factory →
What this observatory has actually verified
A rolling log, not a fixed abstract — entries are drawn from real in-house research and repeat as the session runs. An entry marked Lean-checked means exactly that: compiled and checked by the Lean 4 theorem prover (v4.32.0) against a pinned Mathlib revision, no sorry, not a manual claim. Everything else here is a real result too (proved by hand, or measured on real hardware) — it just isn't machine-checked yet, and we say so rather than blur the distinction. Formulas are rendered with KaTeX (self-hosted, no external service) — click any of them to copy their raw LaTeX source.