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. Jobs run one at a time in submission order, with three admitted uploads per GitHub account per UTC calendar day. The budget resets at 00:00 UTC, and a rejected job still counts once queued. No pull request is required.
From source to proof object
The public number changes only after both kernels accept.
- 01
Upload source
The server derives your author identity and a strict manifest, then atomically archives the encrypted source when the queue admits it.
- 02
Verify in E2B
A durable FIFO starts exactly one no-egress VM checker at a time, then checks statement equality, permitted axioms, Lean, and independent nanoda replay.
- 03
Publish evidence
A passing result is bound to the exact source digest before it can enter the public record.
Keep the signatures. Replace every sorry.
The form supplies your exact rational. Submit only this Lean file; helper declarations and extra imports must live in it. The server generates the manifest and both κ definitions.
- Exactly three required theorem declarations
- One UTF-8 Lean file, at most 2 MB
- No
sorry, custom axioms, or RH assumption
/-
Riemann.fail one-file submission starter
The submission form supplies the exact numerator and denominator. The verifier
then generates currentRecordKappa and candidateKappa for this file.
Before submitting:
1. Keep all three theorem names and statements exactly as written.
2. Replace every sorry with a complete proof. Any remaining sorry is rejected.
3. Put any helper declarations and additional imports in this same file.
4. Do not assume the Riemann hypothesis or add new axioms.
Rate limit: three admitted uploads per GitHub account per UTC calendar day,
resetting at 00:00 UTC. Once an upload enters the verification queue, it uses
one slot even if it later ends in a compilation error, comparison or kernel
rejection, timeout, or infrastructure failure. Validate locally first whenever
possible.
-/
/- Trusted statement generated for one Riemann.fail candidate. -/
import ChallengeDeps.CandidateSpec
noncomputable section
/-- The submitted bound is strictly larger than the current formal record. -/
theorem candidate_strict_improvement :
currentRecordKappa < candidateKappa := by
sorry
/-- The candidate proves a larger unconditional critical-line proportion on dyadic windows. -/
theorem candidate_critical_line_bound :
∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
(candidateKappa - ε) * (Ncount T (2 * T) : ℝ) ≤ N0star T (2 * T) := by
sorry
/-- The same unconditional bound in cumulative windows. -/
theorem candidate_critical_line_bound_cumulative :
∀ ε > 0, ∃ T₀ : ℝ, ∀ T ≥ T₀,
(candidateKappa - ε) * (Ncount 0 T : ℝ) ≤ N0star 0 T := by
sorry
end
A slot is charged only after an upload enters the durable FIFO. From that point every outcome counts—including Lean errors, statement or axiom mismatch, kernel rejection, timeout, and sandbox expiration. Requests rejected before queue admission do not consume a slot, and admitted slots are not automatically refunded.
- Used
- Sign in to view
- Reset
- 00:00 UTC
- Queue
- 1 verifier at a time
Submit a real record improvement
This form consumes a daily slot after queue admission. The complete 1/3 → 2/3 test proof belongs in the noncompetitive flow-test lane above, not here.
2 - 1 / cMTSign 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.
- Starter available above
- Lean source only
- 2 MB maximum
- 3 admitted uploads per account per UTC day
- FIFO · 1 verifier at a time
- Apache-2.0