Riemann zeta function
Submit a formal improvement

Upload a Lean proof for verification.

Enter an exact rational and paste or upload your Lean source. A private E2B sandbox rechecks the fixed theorem with Comparator, the Lean kernel, and nanoda. No pull request is required.

The process

From source to proof object

The public number changes only after both kernels accept.

  1. 01

    Upload source

    The server derives your author identity and a strict manifest from the signed GitHub session.

  2. 02

    Verify in E2B

    A no-egress VM checks statement equality, permitted axioms, Lean, and independent nanoda replay.

  3. 03

    Publish evidence

    A passing result is bound to the exact source digest before it can enter the public record.

Direct verifier

An exact score and a Lean entry file

Current formal record2 - 1 / cMT

Sign in before uploading proof code

The authenticated GitHub login becomes the immutable public author field.

Browser checks are only a preview.

Exact acceptance is recomputed inside the isolated, pinned environment; the checks shown here do not determine the result.