Lean run · strict prime bound
Failed Lean run: strict prime bound
The local Lean check failed because the direct witness only gives a non-strict bound. The theorem remains established.
Typecheck failed
Result and scope
Machine checking, source alignment, reproduction, and review are separate assessments.
Target statement
- Lean check
- Lean typecheck failed locally
- Statement alignment
- Linked by OpenMath staff; review pending
- Independent reproduction
- Not yet reproduced
- Mathematical review
- Independent review pending
Reproduce locally
From the openmath repository root, run the Lean file against the pinned mathlib revision.
cd fixtures/phase0/lean
lake update
lake exe cache get
lake env lean PrimeStrictBroken.lean
lake update
lake exe cache get
lake env lean PrimeStrictBroken.lean
Expected outcome: a nonzero exit at the known proof gap.
Strict-bound task and known failurePrime numbers do not run out · lines 21–25Technical record
Exact identifiers and environment details for auditing or reuse.
Input, toolchain, and record digest
- Run ID
- run-strict-broken
- Input file
- lean/PrimeStrictBroken.lean
- Input SHA-256
- 09f6c5028086b2acee711755f2905570bc432194944846dea2556fb6e62e49ab
- Mathlib commit
- 32d24245c7a12ded17325299fd41d412022cd3fe
- Lean toolchain
- leanprover/lean4:v4.27.0-rc1
- Exit code
- 1
- Diagnostic
- hbound has type n ≤ p but is expected to have type n < p
- Verification ID
- verification-strict-broken
- Record SHA-256
- 766ba956ddefe9dee6120099c80cd8a5c324240f8be04192fbeace7a0897a960
This observation is unsigned, has no digest-pinned container, and has not been independently reproduced. Launcher: lake env lean in a local project with the pinned mathlib revision.