Lean run · strict prime bound
Passing Lean run: strict prime bound
The pinned Lean file typechecked locally. This result applies to the formal statement and exact input shown below.
Typecheck passed
Result and scope
Machine checking, source alignment, reproduction, and review are separate assessments.
Target statement
- Lean check
- Lean typecheck passed 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 PrimeStrict.lean
lake update
lake exe cache get
lake env lean PrimeStrict.lean
Expected outcome: exit code 0 with no Lean diagnostics.
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-success
- Input file
- lean/PrimeStrict.lean
- Input SHA-256
- ceb85a78b5086e78ae29195528323cd7cb1ae880f58958865973b5a931a9da10
- Mathlib commit
- 32d24245c7a12ded17325299fd41d412022cd3fe
- Lean toolchain
- leanprover/lean4:v4.27.0-rc1
- Exit code
- 0
- Diagnostic
- No Lean diagnostics; process exited 0.
- Verification ID
- verification-strict-success
- Record SHA-256
- 303910995ec7de534f973b87ce237174b0494804b0207f22466dcd9958f6d040
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.