Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 7
is no: there is no finite covering system with pairwise distinct odd moduli
greater than one. Jinook Lee posted the claim on the problem's discussion
thread on 2026-05-02 as a five-page note, The Erdős–Selfridge conjecture
via sieve monotonicity, announced as a proof of the conjecture, with a
Lean 4 development (ErdosSelfridge_v11.lean) deposited the same day on
Zenodo (record 19982394, version 1.1, described there as sorry-free with three
axioms taken from Balister, Bollobás, Morris, Sahasrabudhe and Tiba) and pinned
above at the repository's commit of that day. The argument asserts that moduli
with repeated prime factors make covering harder than square-free moduli, so
that the sieve criterion which excludes odd square-free coverings on
their claim page
extends to every configuration of odd moduli. The note names Aristotle as the
system that audited the development.
Depends on. Nothing in this wiki. The development encodes the square-free theorem of Balister, Bollobás, Morris, Sahasrabudhe and Tiba as an axiom rather than importing a proof.
Standing. Rejected. On 2026-05-06 Nat Sothanaphan showed on the thread
that the axiom bbmst_sf_lt_one is false as encoded: the sieve product it
bounds has every factor greater than one, so it always exceeds one, while
the axiom asserts that it is less than one, and the cited Theorem 1.1 of the
square-free paper states only that some modulus of a distinct square-free
covering is even. The author conceded the same day that the axiom is false
under the definition used, since the formalization omitted a constant, and
announced a revision. On 2026-05-07 the site's curator, Thomas Bloom, ruled
the approach flawed, closed the thread to further technical discussion of
the development and allowed only a complete, self-contained Lean
formalization without sorry or axioms appealing to external work to be
posted about it. The community database's ledger of AI contributions marks
the attempt as an incorrect proof. The repository's later versions keep
axioms attributed to the square-free paper and are not a new claim. The
site's label for the problem is VERIFIABLE.