erdős #12
Let be an infinite set such that there are no distinct such that and . Is there such an withDoes there exist some absolute constant such that there are always infinitely many withIs it true that
Worked, still open.
number theory · open · formalized (Lean) · 0 attempts
machinery: divisor-sum-free-set,consecutive-integer-window,Behrend-density,additive-combinatorics,prime-distribution,unit-fractions,explicit-construction-witness
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
alphaproof · AlphaProof Nexus (DeepMind) · machine-verified (Lean)
Machine-verified Lean proof (kernel-checkable, sorry-free).
Lean proof ↗unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Call such a set (A\subset\mathbb N) a **$P$-set** (this is standard terminology): no element (a\in A) divides $b+c$ for two *larger* distinct (b,c\in A).
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 · textbook, ams 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/2663234a28260853790aa5752d8d4550ff0ab1ca/formalconjectures/erdosproblems/12.lean#l39" (literature)
theorem isGood_example :
IsGood {p ^ 2 | (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : p.Prime)}formal-conjectures/12.lean ↗Kernel-checked proof; human-attested statement.
- faithful — reviewer:will-blair
erdos_12.parts.i.lean
status
open