Take this check

Compare the formal theorem and definitions with the informal n = 8 claim.

ErdősProblems.com #132 · task erdos-132-lean-correspondence

Check category: Statement
Task type: Statement audit
Entry points: formalization/ and the n = 8 theorem in the PDF
Source PDF: Download the exact manuscript
Erdős Problem #132, n = 8 proof writeup · version 5d3faea03531…
Effort: about 60 minutes (estimated by significance-editor)
Prerequisites: Lean 4 and the repository's formalization directory

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.

Start a public comment thread

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-132-lean-correspondence
task_id: erdos-132-lean-correspondence
reviewer: '[your name or handle]'
scope: Compare the formal theorem and definitions with the informal n = 8 claim.
manuscript_sha256: 
  5d3faea03531035426c9f5ca8ece9c8db90ff2cdaff4238f3eb1090747c5b209
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]'