Open work
A task someone can pick up.
These are bounded checks recorded by the claimants or editors. Choose one task, follow its instructions, and report what you found. The list is not a ranking of claims.
-
Reproduce the pinned Lean release and report the build and certificate result within the published-cache replay trust boundary.
Check out tag v1.0.5-kernel at commit bb8e1b10b006…. Download all 75 cache-shard ZIP files together with the manifest and checksum assets, place them in one directory, and run python -B scripts/install_release_cache.py --asset-dir <download-directory> --prepare-dependencies --kernel --memory-mib 32768. Do not run lake update. Record the toolchain, commands, result, resource limits, and log hash. This checks reproducibility, not the truth of the mathematical claim.
-
Read one certificate-generation path and record the exact passages followed.
Follow this concrete declaration path from paper/theorem-map.json: Erdos848.PaperGeneratedCertificateProvider.all_N -> numericalCertificates.fiveSharp -> GeneratedTailR263EvenOneFinite23.sharpCertificate -> E1Finite23SharpCertificate -> e1FiniteSharpFourLeafPasses_sound -> erdos848FiveToTenMillionClose -> PaperCertificateProvider.fiveToTenMillion. Record the exact declarations and commands checked, without rating the whole proof.
-
Compare the paper's exact all-N statement with the pinned Lean declaration, recording both the paper version and the pinned machine-proof version.
Record the paper version and the pinned machine-proof version, list the definitions and declarations compared, and record any remaining correspondence question; do not characterize the whole proof. The author reports that editorial revisions after v1.0.5-kernel did not change the theorem, Lean source tree, theorem map, or mathematical conclusion; that report is not an independent finding.
-
Independently build the Theorem D Lean targets and run their axiom audit at commit 3635e74826a4c1fcece7d1cd2b6fa75e43a00510.
Clone github.com/… check out 3635e74826a4…, and retain the pinned lean-toolchain and lake-manifest.json. Run lake exe cache get, lake build Solution Solution.Multiplicity, then lake env lean comparator/PrintAxioms.lean and lake env lean comparator/PrintAxioms/Multiplicity.lean. Report commands, platform, exit codes, and the SHA-256 of the complete log.
-
Compare paper Theorem D with the trusted comparator statement montgomery_taylor_on_critical_line and its counting definitions.
Use page 21 of the paper with SHA-256 6792988e6cd0…. At the pinned repository commit, inspect comparator/ChallengeDeps.lean, comparator/Challenge.lean, comparator/Solution.lean, and config.json. State whether the interval conventions, multiplicity, critical-line count, limit formulation, and constant match; identify every mismatch or unresolved definition explicitly.
-
Assess the passage from Weil-form signature data to the lower bound in Proposition 4.4 and Theorem D, against the pinned paper.
Work from the paper hash recorded here and name that hash in the report. Focus on the off-critical-line block decomposition, tail control, and use of the unconditional prime-side second moment. Name the first step you cannot justify, or state the bounded portion you checked; do not give a paper-wide score.
-
Check the n = 8 geometric deduction only; report the exact passages followed and any first unresolved step.
Use the pinned PDF. Check the profile reduction, both seven-point deletions, the overlap lemma, and the final contradiction. Do not rate the whole paper.
-
Compare the formal theorem and definitions with the informal n = 8 claim.
List the declarations compared and record where correspondence is clear or remains open; do not infer proof correctness from compilation.
-
Trace the declaration chain between manuscript Theorem 1.1 and the Comparator target exists_finitelyPresented_nonsofic_group.
Read Theorem 1.1 on page 78 of the manuscript hashed in this record (sha256 f318c6508c9d…), then read SoficGroups.SourceTopLevelCompressionFinal.exists_finitelyPresented_nonsofic_group, the declaration ComparatorChallenges/D_NonSoficGroup.json names at the pinned commit. Walk the declarations between them and write down each one. The specific thing to look for: the manuscript states a property of one concrete group, the formal target states that some finitely presented group exists. Say where those two part company, and whether anything in between closes the gap.
-
Assess the expander-matching criterion in Proposition 2.3 or the Thompson-group step in Proposition 3.2, naming the exact artifact revision reviewed.
Pick one: the expander-matching criterion in Proposition 2.3, or the Thompson-group step in Proposition 3.2. Work from the manuscript hashed here (sha256 f318c6508c9d…) and name that hash in what you write, so the assessment stays attached to the revision you actually read. "I could not follow step 4" is a useful report and will be recorded as what it is: your reading, signed by you.
-
Check Theorem 1.1 and the Section 3 deduction from the incidence bound to the exponent.
Use the exact PDF in manuscript.url. Check the low-R center selection, the bounds M <= T and L <= T^2, the terms used from Theorem 2.2, and the optimization that gives beta(alpha) and theta. Report the first step you cannot justify, or say which bounded steps you followed; this is not a review of the whole paper.
-
Check the hypotheses of Theorem 2.2 where it is applied to the constructed circles.
Check that the circle family and selected centers satisfy the exact distinctness, multiplicity, and range assumptions of the cited Pach--Tardos incidence theorem. Record the numbered passage examined; do not infer that the main theorem follows from this check alone.
-
Check one short structural result: Proposition 2.1 or Theorem 6.2.
Choose one result, state the exact statement and pages read, and record the definitions and inequalities you checked. A bounded report records only that passage; it is not a verdict on the paper.
-
Check Hypothesis 3.1 and Remark 3.2 against the cited literature.
Use the exact PDF in manuscript.url. Compare the interval, exp(P^c) range, C^3 norm, and error term with the cited Matomaki--Radziwill-- Shao--Tao--Teravainen result. Record whether the paper labels its hypothesis as conjectural and does not present the citation as a proof of it; this is a source-and-scope check, not a proof verdict.
-
Check Lemma 3.3, Proposition 5.1, and Corollary 5.2.
Check the partial-summation step, the smooth approximation and boundary error, and the parameter ranges used to pass from dyadic blocks to the intermediate scales. Record the first gap or the bounded steps followed; do not rate the rest of the manuscript.
-
Check Lemma 6.1 and the decomposition used in the proof of Theorem 1.1.
Follow the split at the polylogarithmic cutoff Y for small, intermediate, and large primes. Check how Lemma 6.1 supplies the cancellation and whether the three errors combine to O(log log log n). Report only the passages read, not a whole-paper conclusion.
-
Optionally check Hypothesis 8.1 and Proposition 8.2.
Verify that the exponential-sum hypothesis has the stated frequency range and norms, and that the argument really implies Hypothesis 3.1. Treat the result as a separate bounded implication; it does not make the hypothesis known.