Take this check

Independently replay the pinned Lean verifier and document the final theorem's actual axiom and dependency boundary.

ErdősProblems.com #1095 · task erdos-1095-lean-reproduction

Check category: Formalization
Task type: Reproduce build
Entry points: verify.sh; AxiomAudit.lean; lake-manifest.json
Source PDF: Download the exact manuscript
A least-common-multiple bound for the Erdős–Selfridge function (pinned PDF) · version 7621e3c47277…
Code: Open the formalization repository · pinned commit e06b3e658c48…
Effort: several hours, dependent on cache availability and hardware (estimated by significance-editor)
Prerequisites: Lean 4.27.0; Pinned Mathlib/PNT dependencies; Isolated build and axiom auditing

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.

Illustrative partial attempt — fictional paper and references:

"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."

This is a useful starting point for a question or partial attempt. It names the scope, the source version, and the specific location. It does not claim the proof is wrong. It identifies an unresolved 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.

Ask about this task

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 partial attempt

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.

Submit your attestation

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

Task status tracks participation, not whether the claim is true. Each report below is limited to the scope its author describes.

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.

Open task discussion

GitHub may require an account to post. To add a scoped check to the record, use the attestation form above.

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.

Open attestation form

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-1095-lean-reproduction
task_id: erdos-1095-lean-reproduction
reviewer: '[your name or handle]'
scope: Independently replay the pinned Lean verifier and document the final 
  theorem's actual axiom and dependency boundary.
manuscript_sha256: 
  7621e3c47277464e64a09bf78515f7a9be621457b4f2d7e6851a18c1564d3d55
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]'