Is it true that for every there exists such that

verified — A frozen deterministic verifier re-checked the claim and passed.verifiedThe problem is open. The best result here is machine-verified: verified reduction, re-checked by an independent verifier.

number theory · open · formalized (Lean) · 1 attempt

use this data

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

Ways to settle this problem3

Each route names what would count as a proof and how it would be checked.

  • dead ends1 · 50%
  • open1 · 50%
verified — A frozen deterministic verifier re-checked the claim and passed.

Verified computationverified_computation · python:verify_396_sieve_certificate.py

sieve lower-bound certificate re-check (pinned tier: scripts/requirements-verifiers.txt)

claimed — no verifier run, no signed judgment

A full formal proof checked by the Lean kernelformal_proof · lean

Lean patch building clean under the math CI profile (no sorry, no new axioms)

banked — A closed route or proven obstruction, kept at full ink as a result.

Obstruction reportobstruction_report · review

precise, artifact-backed reason a route cannot work

Proven dead ends1

Knowing what can't work is a result — kept on record at full ink.

banked — A closed route or proven obstruction, kept at full ink as a result.

Open tasks1

What's still unproven here, ranked by how much depends on it.

claimed — no verifier run, no signed judgment
deps1

Evidence1

verified reduction

machine-verified

Erdos #396: verified REDUCTION. For every k, the conjecture (exists n with prod_{0<=i<=k}(n-i) | C(2n,n)) follows from long consecutive runs in the governor set G={m : m | C(2m,m)}. Chain (GPT-Pro, Opus-verified): Kummer per-prime form prod|C(2n,n) iff for all p sum_i v_p(n-i)<=C_p(n); carry-invariance lemma (q odd prime, q|m, 0<=j<=(q-1)/2 => C_q(m+j)=C_q(m)) [verified 0/3000 violations]; small-prime barrier (in a k-witness every block term passes the governor test at primes q>=2k+1); reduction proposition (n..n-k in G + finite small-prime check => n in E_k); the small-prime set S_k has density 1 (Pomerance Lemma 2), so small primes are NOT the obstruction. Density: E_k subset {n: P+(n),P+(n-1)<=sqrt(2n)} giving upper-log-density <= (1-log2)^2 ~ 0.094 (Teravainen, arXiv 1710.01195) < governor density 0.11425 (Ford-Konyagin, arXiv 1909.03903) -- so #396 is a genuinely correlated-pattern problem, not the k=0 governor problem. Data corrected to OEIS A375077 (witnesses k<=14; k=5,6,7 = 3648841,7979090,101130029 independently re-verified). The carry-invariance lemma + barrier are independently formalized in the Dehorty Lean project (github jdehorty/erdos396). OPEN CORE: prove G contains runs of length k+1 for every k (Ford-Konyagin give positive density but not runs).

{"reduces_to":"consecutive runs in G={m | C(2m,m)}","verifier":"scripts/verify_396_reduction.py","carry_invariance":"verified 0/3000","witnesses":"A375077 k<=14; k=5,6,7 re-verified","governor_runs...

depends on (the wall): scripts/verify_396_reduction.py

claimexact_arithmetic_recompute · scripts/verify_396_reduction.py — Opus 4.8exact_arithmetic_recompute · script…Opus 4.8literature_corroboration · oeis-A375077+ford-konyagin+teravainen+dehorty — Opus 4.8literature_corroboration · oeis-A37…Opus 4.8exact_arithmetic_recompute · opus_396_sharpening — Opus 4.8exact_arithmetic_recompute · opus_3…Opus 4.8exact_arithmetic_recompute · opus_396_sieve_certificate — Opus 4.8exact_arithmetic_recompute · opus_3…Opus 4.8exact_arithmetic_recompute · opus_396_obstruction_map — Opus 4.8exact_arithmetic_recompute · opus_3…Opus 4.8

scripts/verify_396_reduction.py + citation checks (OEIS/arXiv/GitHub)

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **open** (as far as the current literature indicates).

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

Formal proof

AMS 11 · open (literature)

theorem erdos_396 : answer(sorry) ↔ ∀ k : ℕ, ∃ n : ℕ, descFactorial n (k + 1) ∣ centralBinom n
formal-conjectures/396.lean ↗

OEIS1

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Verify this yourself

Run this command — the output must match these fingerprints.

vela reproduce examples/erdos-problems
  • packet.json · sha256 537cb914c2fb31d5e8783be4ae1f024a7532cfd5106b4a05d9bf29feb1c0814b

Search Vela

Search problems, results, contributors, and pages — or jump straight to an id.