Task · formalization exercise
Formalize a prime strictly above every bound
Produce a Lean declaration for a known corollary and explain why the bound must be shifted by one. The task and its sample attempts are reference data.
Known result · sample task
Target statement
The deliverable is a declaration and a short source-grounded explanation.
∀ n : ℕ, ∃ p, n < p ∧ Nat.Prime p
The pinned theorem supplies a prime at or above its input. This task asks for a prime strictly above the original bound.
Strict-bound task and known failurePrime numbers do not run out · lines 21–25Known failed route
Applying
Nat.exists_infinite_primes n yields n ≤ p, which is too weak for n < p.The failed attempt is included in the starting context so the obstruction is visible before the follow-up.
Inspect failed run →Context packs
Each pack is an immutable snapshot of selected sources and prior work for this task.
Version 1 · starting contextSource, related claims, proof idea, and failed attempt.
Open v1 →Version 2 · after the follow-upAdds the passing local run and preserves the earlier failure.
Open v2 →Acceptance criteria
- Typechecks under the pinned Lean/mathlib toolchain.
- Uses the existing theorem without claiming mathematical novelty.
- Explains why applying the theorem at n is too weak and n + 1 succeeds.
- Keeps source alignment, machine checking, and human review as separate states.