erdős #686
Can every integer be written asfor some and ?
Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.
number theory · open · formalized (Lean) · 1 attempt
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
partial proof
machine-sealed
Erdos #686: lean/Vela/Erdos686.lean (kernel-checked, axiom-clean, no sorry) proves the k=2 and k=4 obstructions for prime-power squares. If A is a prime power then A^2 has no representation N=prod_{i<=k}(m+i)/prod_{i<=k}(n+i) (m>=n+k) with k=2 or k=4 -- in particular N=4 has none -- via prime-power divisibility (no multiple of A lies strictly between consecutive multiples A*N0 and A*(N0+1)) plus a general k=4 => k=2 reduction with the same multiplier ((t+1)..(t+4)=4*(u+1)(u+2)). This is theorem-grade partial progress; it does NOT address k=3, k>=5, or composite non-prime-power square N.
{"lean_file":"lean/Vela/Erdos686.lean","theorems":["Vela.Erdos686.no_prime_power_square_consecutive_product","Vela.Erdos686.no_k2_prime_power_square","Vela.Erdos686.no_k2_four","Vela.Erdos686.four_...
depends on (the wall): lean/Vela/Erdos686.lean
lake build Vela.Erdos686 (green, axiom-clean, no sorry)
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Take [ k=2N-2,\qquad n=-2N,\qquad m=2. ] Then (k\ge 2) for (N\ge 2), and [ n+k=-2N+(2N-2)=-2\le 2=m, ] so the condition (m\ge n+k) holds. Also none of the factors $n+i$ is $0$, since $n+i$ runs from $-2N+1$ up to $-2$.
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_686 :
answer(sorry) ↔ ∀ N ≥ (2 : ℕ), ∃ᵉ (k ≥ 2) (n : ℕ) (m ≥ n + k),
(N : ℚ) = (∏ i ∈ Finset.Icc 1 k, (m + i)) / (∏ i ∈ Finset.Icc 1 k, (n + i))formal-conjectures/686.lean ↗Vela formalization: Erdos686Tail.lean (sorry-free), Erdos686.lean (sorry-free)
status
open