Riemann zeta function
Verification methodology

How submissions are verified.

Acceptance is a deterministic formal check, so the process runs without any human judgment of the argument itself.

Kernel verifiedExact statement · permitted axioms · isolated replay
How verification works

How a submission is checked

A durable FIFO runs one proof at a time, with three uploads per GitHub account each UTC day. Acceptance depends only on the automated check; expert review is recorded separately.

  1. 01

    Upload one Lean file

    Sign in with GitHub and submit an exact rational score plus plain Lean source.

  2. 02

    Fix the statement

    The build generates the theorem from trusted templates. A submission cannot change the definitions or hypotheses.

  3. 03

    Recheck the proof

    Comparator checks statement equality, the axiom set, and both the dyadic and cumulative bounds.

  4. 04

    Replay in two kernels

    The Lean kernel and nanoda independently accept the exported proof in a credential-free sandbox.

  5. 05

    Publish the record

    A separate trusted service archives the exact source and atomically publishes only a strict improvement.

Separation of duties

Verification and publication use separate trust domains

Untrusted Lean and the credentialed publisher are separated so proof code can never read or use a write credential.

Candidate sandbox

Checks one server-generated manifest and one Lean file in a private, no-egress E2B environment with no application credentials. Queue admission separately seals the exact source in the maintainer archive.

no secrets

Comparator

Reconstructs trusted declarations and rejects any proof whose statements differ, even if the names match.

no secrets

Publisher

Rehashes the sandbox source and attestation, then atomically publishes accepted evidence and updates the ledger without a pull request.

write after pass
Two independent kernels

Independent replay narrows the trusted computing base.

Lean elaborates source code into a compact proof object, which the Lean kernel checks first. Comparator then exports that object, and nanoda, a separate small implementation, checks it again. A bug in one checker is not enough to advance the record.

Lean sourceLean kernelexportnanoda
Permitted axioms

The permitted axioms

  • propext
  • Quot.sound
  • Classical.choice

Any additional transitive axiom rejects the submission.

Untrusted-code model

Elaborating a Lean proof runs code, so the verifier treats every submission as untrusted.

Formal correctness does not imply the code is safe to run, so resource limits and filesystem isolation protect the runner while the kernels protect the theorem.

No outbound networkDependencies are pinned into the template before untrusted code runs, and a live probe must confirm that egress is disabled.
Credentials absentThe verifier cannot publish, push, or read application secrets.
Resources boundedCPU time, memory, processes, and writable paths are restricted.
Reproduce the check

Run the verifier yourself.

The tool installer checks out every verifier component at the commit recorded in the challenge contract.

Prepare your submission
Linux verifier runner
npm ci
tools_dir="$(mktemp -d)"
bash scripts/install-verifier-tools.sh "$tools_dir"
export COMPARATOR_BIN="$tools_dir/comparator/.lake/build/bin/comparator"
export COMPARATOR_LANDRUN="$tools_dir/landrun/landrun"
export COMPARATOR_LEAN4EXPORT="$tools_dir/comparator/.lake/packages/lean4export/.lake/build/bin/lean4export"
export COMPARATOR_NANODA="$tools_dir/nanoda/target/release/nanoda_bin"
npx tsx scripts/verify-submission.ts submissions/<id> --mode=full