erdős #7
Is there a distinct covering system all of whose moduli are odd?
Open — best to date is a honest null, not yet sealed.
number theory · open · formalized (Lean) · 1 attempt
machinery: covering-system,odd-moduli-covering,BBMST-sieve-density,LP-layered-deletion,antichain-divisibility-reduction,prime-power-modulus-monotonicity,finite-witness-verifiable,lcm-divisibility-constraint
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
honest null
needs verification
attempted via frontier 'difference/covering' (transfer_strength=partial) -> no_progress
No solve/partial on this pass. Transfer into the owned frontier was 'partial'. Do not re-attack cold; needs a new idea or richer accumulated context.
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
It depends on whether you require the moduli to be **distinct** (which is the nontrivial version people usually mean).
candidate solution ↗llm-hunter · codex 5.2 extra high, gpt 5.2, gpt pro 5.2 · unverified
4 LLM attack(s) recorded (codex 5.2 extra high, gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_7 : answer(sorry) ↔
∃ (C : StrictCoveringSystem ℤ), ∀ i,
¬ C.moduli i ≤ Ideal.span {2} ∧ C.moduli i ≠ ⊤formal-conjectures/7.lean ↗status
open