Experiments that are running, and what they have produced so far.

The fact this rests on. Searching is expensive and checking is nearly free. Finding a factorisation, a proof term or a descent costs orders of magnitude more than confirming one. A browser cannot compete with a GPU at searching — but it can check a certificate in less time than it spends laying out this paragraph. Everything below follows from that asymmetry and nothing below requires you to donate processing time.

Why it is worth doing at all. A result checked by ten thousand independent machines, across ten thousand browsers and arithmetic implementations, is a different object from one we checked once ourselves. That is the replication argument, and it is the only reason anyone believes an experimental result. One of us checking a thing carefully is evidence. Ten thousand strangers checking it independently is a different kind of evidence.

Check one yourself, and watch what it cost

Below is a real certificate: a range of integers and a claimed value of M(n) = Σ_k≤n μ(k), the Mertens function — the same object the strip along the bottom of every page draws, and the subject of one of our own deposited papers. Verifying it means recomputing μ over the range and comparing. Finding an interesting range is work; confirming one is arithmetic.

What we will not claim until we have measured it

The obvious pitch for this is “advance mathematics with no environmental cost”, and it is not one we have earned. An idle processor draws less power than a busy one, so the marginal cost of a verification is small, not zero, and the difference between those two words is the difference between a measurement and a marketing claim. This page therefore publishes no energy figure. What it shows is the time your own browser took, next to something you can compare it against. When there is a defensible energy number measured on real hardware, it will appear here with the method beside it.

The rules, because someone already ruined this idea

In-browser cryptocurrency mining destroyed trust in anything that touches a visitor’s processor, and it deserved to: it took people’s electricity without asking and hid that it was doing so. So this runs the other way round, and these are not preferences.

• Nothing runs until you ask. No idle-time scavenging, no work on page load. The buttons above are the only trigger.
• Bounded. One certificate, or a hundred if you choose. There is no mode where it keeps going.
• Measured in front of you. The cost is shown in the same panel that does the work, not in a footnote.
• Auditable. When results are recorded, the ledger will be public and hash-chained like the rest of this site, so a verification cannot be quietly invented or removed — including by us.
• If it ever needs hiding, it is wrong.

Where this is

Today this is the client half: a real certificate, really verified, really timed, in your browser. What does not exist yet is the half that matters most — certificates drawn from work we actually need verified, and a public chained ledger of who verified what. Both are designed and neither is built. It is published at this stage on purpose, because an experiment announced only once it works is not an experiment.

And the open question we cannot answer by building harder: whether the thing being verified is worth verifying. A certificate nobody needed is a decoration with an energy cost, however small. The 16 proved findings still sitting undeposited (the count is computed on /publications, not typed) are the candidate list, and choosing among them is a mathematical judgement rather than an engineering one. The four records the Lax Lean Archive registered on 18 September 2026 are the other candidate: 42 statements whose proofs the archive already rebuilt with Lean’s kernel, which is exactly the kind of certificate this page is built to check.