Help check a claim

Pick one. Read the passage. Report what you find.

Each task is scoped to a single passage or artifact. Reading needs no account; submitting through GitHub requires one.

open

Compare the graph and path conditions in Section 1, Problem 1212,...

ErdősProblems.com #1212

Type: Statement audit Check: Statement Prerequisites: Section 1 of the paper; the repository README and the two named Lean files Effort: about 1–2 hours for someone comfortable reading Lean statements
open

Read one certificate-generation path and record the exact passages followed.

ErdősProblems.com #848

Type: Read check Check: Proof step Prerequisites: Paper definitions and finite certificate format Effort: about 60-90 minutes
open

Reproduce the pinned Lean release and report the build and certificate...

ErdősProblems.com #848

Type: Reproduce build Check: Formalization Prerequisites: Lean and the repository's pinned release instructions Effort: about 2 hours for the published-cache replay; a fresh source build is separate and may take multiple days
open

Compare the paper's exact all-N statement with the pinned Lean declaration,...

ErdősProblems.com #848

Type: Statement audit Check: Statement Prerequisites: the paper theorem map and Lean declaration names Effort: about 45 minutes
open

Independently build the Theorem D Lean targets and run their axiom audit at...

Significance editor

Type: Reproduction Check: Computation Prerequisites: Lean command-line use and the pinned repository toolchain Effort: about 60–90 minutes with the repository cache; longer if dependencies must build from source
open

Compare paper Theorem D with the trusted comparator statement...

Significance editor

Type: Correspondence Check: Statement Prerequisites: Lean source reading and the paper's counting notation Effort: about 60–90 minutes
open

Assess the passage from Weil-form signature data to the lower bound in...

Significance editor

Type: Mathematical review Check: Proof step Prerequisites: Analytic number theory and the paper's Weil-form notation Effort: about 3–5 hours
taken

Produce a shorter human-readable exposition separating the new tilted sieve...

ErdősProblems.com #4

Type: Exposition Check: Exposition Prerequisites: FGKMT 2018 and the tilted-sieve argument in Sections 3–5 Effort: O(1) months, as publicly anticipated by Ben Green
open

Reproduce the completed tilted-sieve theorems and guarded axiom output at...

ErdősProblems.com #4

Type: Reproduce build Check: Formalization Prerequisites: Lean 4.33.0, Mathlib 4.33.0, and the pinned src/latest project Effort: [FILL: independent builder estimate]
open

Compare the manuscript's two asymptotic statements with the pinned Lean...

ErdősProblems.com #4

Type: Statement audit Check: Statement Prerequisites: The manuscript definitions of Y(X) and G(T); Lean definitions maximumCoverLength and maximumPrimeGap Effort: about 60–90 minutes for the two final statements
open

Re-derive the finite interval sieve and eventual main-term/error comparison...

ErdősProblems.com #1095

Type: Read check Check: Proof step Prerequisites: Number theory; Chinese remainder theorem; Inclusion–exclusion and asymptotic estimates Effort: about 1–2 hours for a first scoped reading
open

Independently replay the pinned Lean verifier and document the final...

ErdősProblems.com #1095

Type: Reproduce build Check: Formalization Prerequisites: Lean 4.27.0; Pinned Mathlib/PNT dependencies; Isolated build and axiom auditing Effort: several hours, dependent on cache availability and hardware
open

Compare the paper's eventual lcm theorem with both final Lean declarations...

ErdősProblems.com #1095

Type: Statement audit Check: Statement Prerequisites: Paper definition of g; Basic Lean statement reading Effort: about 45–60 minutes
open

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

ErdősProblems.com #132

Type: Statement audit Check: Statement Prerequisites: Lean 4 and the repository's formalization directory Effort: about 60 minutes
open

Check the n = 8 geometric deduction only; report the exact passages followed...

ErdősProblems.com #132

Type: Read check Check: Proof step Prerequisites: Planar distance geometry and the cited seven-point classification Effort: about 90 minutes
open

Trace the declaration chain between manuscript Theorem 1.1 and the...

Significance editor

Type: Correspondence Check: Statement Prerequisites: None listed Effort: Not estimated
open

Assess the expander-matching criterion in Proposition 2.3 or the...

Significance editor

Type: Mathematical review Check: Proof step Prerequisites: None listed Effort: Not estimated
open

Check the hypotheses of Theorem 2.2 where it is applied to the constructed circles.

ErdősProblems.com #653

Type: Read check Check: Proof step Prerequisites: Theorem 2.2 as cited in the manuscript Effort: [FILL: editor estimate]
open

Check Theorem 1.1 and the Section 3 deduction from the incidence bound to...

ErdősProblems.com #653

Type: Rederive Check: Proof step Prerequisites: incidence geometry basics Effort: [FILL: editor estimate]
open

Check one short structural result: Proposition 2.1 or Theorem 6.2.

ErdősProblems.com #653

Type: Bounded structural check Check: Proof step Prerequisites: None listed Effort: Not estimated
open

Compare the note’s main result with Problem 719, explicitly recording the...

ErdősProblems.com #719

Type: Read check Check: Proof step Prerequisites: the exact Problem 719 statement; the note, Zenodo 22568303 version 1.1 (pinned in this record); the references it cites Effort: initial 2–3 hours; a complete verification may take longer
open

Check Hypothesis 3.1 and Remark 3.2 against the cited literature.

ErdősProblems.com #726

Type: Statement audit Check: Statement Prerequisites: Hypothesis 3.1 and the cited literature Effort: [FILL: editor estimate]
open

Check Lemma 6.1 and the decomposition used in the proof of Theorem 1.1.

ErdősProblems.com #726

Type: Main cancellation Check: Proof step Prerequisites: None listed Effort: Not estimated
open

Optionally check Hypothesis 8.1 and Proposition 8.2.

ErdősProblems.com #726

Type: Alternate hypothesis Check: Proof step Prerequisites: None listed Effort: Not estimated
open

Check Lemma 3.3, Proposition 5.1, and Corollary 5.2.

ErdősProblems.com #726

Type: Rederive Check: Proof step Prerequisites: partial summation and smooth approximation Effort: [FILL: editor estimate]

9 derived tasks (records needing exposition)

Derived by the build for records without exposition. An editor fills in details before inviting contributors.

derived

We prove that this graph contains an infinite simple path, answering Erdős...

ErdősProblems.com #1212

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The submission claims a full proof that, for every N >= 1, the maximum size...

ErdősProblems.com #848

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

lim inf as T → ∞ of N₀*(T, 2T) / N(T, 2T) ≥ 3/2 − (1/√2) cot(1/√2) = 0.67250… .

Significance editor

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The paper claims that for every sufficiently large integer k there is an...

ErdősProblems.com #1095

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The submission claims a proof of the first assertion of Erdős Problem #132...

ErdősProblems.com #132

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The unit group L_F2(1,2)× of the binary Leavitt algebra is not sofic.

Significance editor

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The manuscript gives a partial result toward Erdős Problem #653, proving an...

ErdősProblems.com #653

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

For every 3-graph G on n ≤ 9 vertices, |E(G)| − 3ν(G) ≤ ex₃(n, K₄³)....

ErdősProblems.com #719

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]
derived

The paper proves Problem #726 conditionally on an explicitly stated...

ErdősProblems.com #726

Type: Exposition Check: Exposition Prerequisites: None listed Effort: [FILL]

Pick one. Read the passage. Report what you find.

Compare the graph and path conditions in Section 1, Problem 1212,...

Read one certificate-generation path and record the exact passages followed.

Reproduce the pinned Lean release and report the build and certificate...

Compare the paper's exact all-N statement with the pinned Lean declaration,...

Independently build the Theorem D Lean targets and run their axiom audit at...

Compare paper Theorem D with the trusted comparator statement...

Assess the passage from Weil-form signature data to the lower bound in...

Produce a shorter human-readable exposition separating the new tilted sieve...

Reproduce the completed tilted-sieve theorems and guarded axiom output at...

Compare the manuscript's two asymptotic statements with the pinned Lean...

Re-derive the finite interval sieve and eventual main-term/error comparison...

Independently replay the pinned Lean verifier and document the final...

Compare the paper's eventual lcm theorem with both final Lean declarations...

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

Check the n = 8 geometric deduction only; report the exact passages followed...

Trace the declaration chain between manuscript Theorem 1.1 and the...

Assess the expander-matching criterion in Proposition 2.3 or the...

Check the hypotheses of Theorem 2.2 where it is applied to the constructed circles.

Check Theorem 1.1 and the Section 3 deduction from the incidence bound to...

Check one short structural result: Proposition 2.1 or Theorem 6.2.

Compare the note’s main result with Problem 719, explicitly recording the...

Check Hypothesis 3.1 and Remark 3.2 against the cited literature.

Check Lemma 6.1 and the decomposition used in the proof of Theorem 1.1.

Optionally check Hypothesis 8.1 and Proposition 8.2.

Check Lemma 3.3, Proposition 5.1, and Corollary 5.2.

We prove that this graph contains an infinite simple path, answering Erdős...

The submission claims a full proof that, for every N >= 1, the maximum size...

lim inf as T → ∞ of N₀*(T, 2T) / N(T, 2T) ≥ 3/2 − (1/√2) cot(1/√2) = 0.67250… .

The paper claims that for every sufficiently large integer k there is an...

The submission claims a proof of the first assertion of Erdős Problem #132...

The unit group L_F2(1,2)× of the binary Leavitt algebra is not sofic.

The manuscript gives a partial result toward Erdős Problem #653, proving an...

For every 3-graph G on n ≤ 9 vertices, |E(G)| − 3ν(G) ≤ ex₃(n, K₄³)....

The paper proves Problem #726 conditionally on an explicitly stated...