Take this check
Reproduce the pinned Lean release and report the build and certificate result within the published-cache replay trust boundary.
- Check category
- Formalization
- Task type
- Reproduce build
- Entry points
- v1.0.5-kernel release and finite certificates
- Source PDF
- Download the exact manuscript
- Code
- Open the formalization repository · pinned commit
bb8e1b10b006… - Effort
- about 2 hours for the published-cache replay; a fresh source build is separate and may take multiple days
- Prerequisites
- Lean and the repository's pinned release instructions
Why this matters
The question above defines what this investigation can establish. Its findings help the author and future readers understand that specific part of the argument.
After editorial review and your confirmation of the wording, an accepted check is published as a dated, scoped, citable entry that future readers, referees, and the author can point to. Even a partial attempt or a negative result is useful. It tells everyone what has been tried and where the open questions remain.
What a good response looks like
You do not need to write a referee report or certify the whole paper. A useful response describes what you actually did and what you found, scoped to this task.
"I read pages 4-6 of the PDF (version 1 of a fictional paper) and traced the argument from the hypothesis through Lemma 2.3. The deduction on page 5, line 12 appears to use the bound from Lemma 2.1 without verifying that the hypotheses of 2.1 hold in this case. I spent about 20 minutes and did not resolve this step."
Ways to contribute
Choose the level that fits what you have. All three are useful.
- Ask about this step
-
Something is unclear or you want to confirm scope before starting. This helps sharpen the task for everyone.
- Report what you tried
-
You worked on it but reached a stopping point: ran out of time, hit a sub-question you could not resolve, or found the task harder than expected. Recording your attempt can help the next reader choose where to continue.
- Submit a scoped check
-
You completed the stated scope and can report what you found: whether the passage held up, where it did not, or what remains open. An accepted check is published after editorial review and your confirmation.
Your contribution is credited
Published checks retain your name (or handle), the exact scope you checked, the date, and a citable link. Your work appears on the public record alongside the claim. It does not disappear into an anonymous review process. You can correct the wording before it is merged.
Status
Open.
Verification record
No scoped check has been recorded for this task yet.
Comments and questions
Use the public GitHub thread to ask about this task, share a partial attempt, or discuss how to approach it. Discussion is informal and does not become evidence in the claim record.
How to do this
- Download the exact manuscript above and start with the stated entry points. The version hash identifies the file for the eventual record; you do not need to calculate it before reading.
- Read or reproduce only the stated scope and note the method you actually used.
- Submit what you found through the linked attestation form below, using the record, task, scope, and manuscript hash shown here. No Significance account is required; GitHub may ask you to sign in.
Attestation template (for advanced users)
Fill only what you did. State what you checked and found, not whether the whole proof is correct.
id: att-erdos-848-lean-reproduction task_id: erdos-848-lean-reproduction reviewer: '[your name or handle]' scope: Reproduce the pinned Lean release and report the build and certificate result within the published-cache replay trust boundary. manuscript_sha256: 54a910e7bcdaaaf03d24aee2685083f3b14a55be325ce54f6bc18e96bb890a8b asserted_at: '[YYYY-MM-DDTHH:MM:SSZ]' method: '[what you actually did: read / rederived / rebuilt / compared]' finding: '[what you checked and found about exactly this scope]' limits: '[what you did not check — optional but encouraged]'