Open Proof Network

Problems / euclid-primes / review

Formalization review of euclid-primes

“For every natural number n there is a prime greater than n.”

Opened 2026-10-13 by network (network) ; state: needs an intent signer · 1 candidate, 1 cluster, 4 questions waiting. Built from the review’s records only; every table below is derived from them, and nothing here is a verdict: the grade is what was signed. How a statement is reviewed →

1candidate
1surviving
1cluster
4questions waiting
0open pair directions
0 / 4mutants caught

1 · Candidates

Exhibits: kernel-checked results the gate’s job wrote. Only these are evidence for a grade (D-9 v3.12). A candidate’s Lean is shown as written, every type as its author typed it; nothing here was rendered by a model.

Candidate and its LeanAuthorOriginStage-3 result
c-5b109e7f · 2026-10-13
Lean · c-5b109e7f.lean · sha256 5b109e7fcdb6
import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  sorry
curator — a model's: unnamed (other)ported from existing infinitude-of-primessurviving

2 · Pairs and clusters

Exhibits: each direction between two candidates is proved, refuted (a kernel-checked instance) or open, as the pair records say. Both directions proved put two candidates in one cluster; an open direction is claimable work (F26-R8).

1 cluster among the surviving candidates: {c-5b109e7f}.

No pair has been compared yet.

3 · Questions and answers

Judgements: a question is put to the intent signer in mathematics, and an answer is that person’s word, signed through the site and naming their login. An answer becomes an intent test (section 4); an answer that cites no source is flagged. Never evidence for a grade on its own.

  1. q-1 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-a53f17d2), 2026-10-14

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

  2. q-2 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-10a55583), 2026-10-14

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

  3. q-3 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-72a8988e), 2026-10-14

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

  4. q-4 A variant of the statement agrees with it on every small case checked. Is there a case on which the conjecture and this variant should differ?

    raised by a mutant (e-968922ac), 2026-10-14

    Waiting for the intent signer: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

4 · The test matrix

Exhibits: every intent test run against every candidate, kernel-checked, and the mutants of the surviving cluster’s representative the tests caught, as a measure of the tests (F26-R8). No model supplied an expected value: each comes from an answer, a citation or the candidates’ agreement, named per test.

0 of 4 mutants caught by the tests; a mutant every test passed became a question (section 3).

No intent test has been written.

5 · Screens and the brief

Exhibits: the compile and the soundness screens the gate ran on each candidate (D-9 layer 2), kernel-checked. The brief beside them is a model’s judgement and is marked so.

CandidateCheckResultDetail
c-5b109e7fscreenpassnegation: nothing proved within the budget
c-5b109e7fscreenpassfalse: nothing proved within the budget
c-5b109e7fcompilepasselaborates at the pin; small cases do not apply: the claim is a closed proposition, not a predicate on n
Lean · e-ebe0796b.lean · sha256 706d311ee188
-- opn-review: {"cand": "c-5b109e7f", "op": "compile"}
import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

namespace C_c_5b109e7f
/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  sorry
end C_c_5b109e7f

6 · Signatures

Judgements: a signature is a decision written by a person, by role; the page never computes one (D-9 v3.39). The intent signer answers the questions and signs that the surviving cluster says what the conjecture says; the independent signer reads the Lean and signs that the evidence supports it.

Intent signer: empty — may sign: nobody yet: this problem has no steward, so the review needs an intent signer (D-32).

Independent signer: empty — may sign: anyone who reads Lean, wrote no candidate in the surviving cluster and is not the intent signer.