Vela
✦ 5 frontiers

frontiers / frontier

Erdős problems frontier

constellation seal · derived from vfr_37aec80d874a0239
id
vfr_37aec80d874a0239
license
CC-BY-4.0
findings
1,256
accepted core
6
contested
0
links
17
sources
1,234
evidence
1,256
avg conf
0.98

used by 0 · replayed by 2 producers

e1271/1271 · statement.attested · reviewer:will-blair · 2026-06-10 · null→null

Graph

linked findings 32 · links 17 · link types 1

graph

depends17
Erdős Problem #1094 remains OPEN. Statement: For all $n\ge 2k$ the least prime factor of $\binom{n}{k}$ is $\le\max(n/k,k)$, with only finitely many exceptions. Topics: number theory, binomial coefficients. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.1OBLIGATION (Erdos #1094). BANKED: the 14 ELS exceptions enumerated provably-complete to k<=40 (binom_exception_enum). OPEN: extend the complete enumeration / prove finiteness of the exception set for all k.2Erdős Problem #700 remains OPEN. Topics: number theory, binomial coefficients. Erdős prize: no. Not yet formalized in Lean. OEIS: A091963, possible.3OBLIGATION (Erdos #700). BANKED: f(n)=min gcd(n,C(n,k)) recomputed for the cited cases (semiprime and prime-power families). OPEN: characterize f(n) in general beyond the verified families.4Erdős Problem #647 has status 'verifiable'. Statement: Let $\tau(n)$ count the number of divisors of $n$. Is there some $n > 24$ such that $$ \max_{m < n}(m + \tau(m)) \leq n + 2? $$ Topics: number theory. Erdős prize: £25. Statement is machine-verified in Lean (formal-conjectures). OEIS: A062249, A087280.5OBLIGATION (Erdos #647). BANKED: the prime / forced-divisor channel is provably exhausted (banked obstruction_map + Erdos647Obstruction.lean). OPEN: a different channel is required; the prime channel cannot close it (stop grinding it).6Erdős Problem #617 has status 'falsifiable'. Statement: Let $r\geq 3$. If the edges of $K_{r^2+1}$ are $r$-coloured then there exist $r+1$ vertices with at least one colour missing on the edges of the induced $K_{r+1}$. In other words, there is no balanced colouring. A conjecture of Erdős and Gyárfás [ErGy99]. Topics: graph theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.7OBLIGATION (Erdos #617). BANKED: K25 balanced-coloring construction known; the K26 finite case is the first open case and reduces to a SAT instance. OPEN: produce the LRAT/RAT certificate for the K26 SAT encoding and re-check it with `vela reproduce` (unsat_cert); the symmetry-breaking step needs RAT, beyond the current RUP checker.8Erdős Problem #993 has status 'falsifiable'. Topics: graph theory. Erdős prize: no. Not yet formalized in Lean. OEIS: possible.9OBLIGATION (Erdos #993). BANKED: the banked unimodality result for the tree/forest case verified (frozen kernel). OPEN: the general Alavi-Erdos unimodality conjecture is open.10Erdős Problem #488 has status 'falsifiable'. Statement: Let $A$ be a finite set and $$B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}.$$ Is it true that, for every $m>n\geq \max(A)$, $$\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?$$ Topics: number theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.11OBLIGATION (Erdos #488). BANKED: per-fixed-A exact decision certificates (7500+ antichains, zero counterexamples). OPEN: no uniform proof: the per-A certificates do not combine into a statement for all A.12Erdős Problem #396 remains OPEN. Statement: Is it true that for every $k$ there exists $n$ such that $$\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?$$ Topics: number theory, binomial coefficients. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: A375077.13OBLIGATION (Erdos #396). BANKED: the GPT-Pro reduction is banked and re-verified (obstruction map: HONEST, no solve). OPEN: the reduction does not solve #396; the solve remains open.14Erdős Problem #203 remains OPEN. Statement: Is there an integer $m$ with $(m, 6) = 1$ such that none of $2^k \cdot 3^\ell \cdot m + 1$ are prime, for any $k, \ell \ge 0$? Topics: primes, covering systems. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.15OBLIGATION (Erdos #203). BANKED: a partial CRT covering certificate (m + 20 prime rows, ~0.7467 density) verified (crt_partial_cover). OPEN: extend to a full cover (the verified rows do not cover all residues).16Erdős Problem #307 has status 'verifiable'. Statement: Are there two finite set of primes $P$ and $Q$ such that $$ 1 = \left( \sum_{p \in P} \frac{1}{p} \right) \left( \sum_{q \in Q} \frac{1}{q} \right) $$ ? Asked by Barbeau [Ba76]. [Ba76] Barbeau, E. J., _Computer challenge corner: Problem 477: A brute force program._ Topics: number theory, unit fractions. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.17OBLIGATION (Erdos #307). BANKED: the congruence-barrier construction verified. OPEN: the unconditional bound remains open.18Erdős Problem #124 remains OPEN. Topics: number theory, base representations. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.19OBLIGATION (Erdos #124). BANKED: the reservoir criterion verified on the BEGL case {3,4,7}, k=1. OPEN: uniform L-syndeticity across all cases remains open.20Erdős Problem #1093 remains OPEN. Topics: number theory, binomial coefficients. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.21OBLIGATION (Erdos #1093). BANKED: three delta=1 examples beyond ELS93 (k=106/126/129) verified; the density model leans finite. OPEN: prove finiteness of the delta=1 deficiency cases (the density argument is heuristic, not a proof).22Erdős Problem #1056 remains OPEN. Statement: Let $k ≥ 2$. Does there exist a prime $p$ and consecutive intervals $I_0,\dots,I_k$ such that $\prod\limits_{n{\in}I_i}n \equiv 1 \mod n$ for all $1 \le i \le k$? Topics: number theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: A060427.23OBLIGATION (Erdos #1056). BANKED: explicit cut-equality certificates verified for every k in 2..14 (interval_product witnesses). OPEN: the problem asks for EVERY k; a uniform construction or proof for all k remains open.24Erdős Problem #684 remains OPEN. Topics: number theory, primes, binomial coefficients. Erdős prize: no. Not yet formalized in Lean. OEIS: A392019, possible.25OBLIGATION (Erdos #684). BANKED: f(M_K-1) > K verified for K=3..12 via Kummer no-carry (effective, subsequential lower bound). OPEN: promote the subsequential bound to the full claim for all n.26Erdős Problem #699 has status 'falsifiable'. Statement: **Erdős Problem 699.** Is it true that for every $1 \le i < j \le n / 2$ there exists a prime $p \ge i$ with $p \mid \gcd\big(\binom{n}{i}, \binom{n}{j}\big)$? Topics: number theory, binomial coefficients. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: N/A.27OBLIGATION (Erdos #699). BANKED: the central-doubling reduction + CRT obstruction verified; the two arms provably do not meet. OPEN: the gap between the arms is the open obstruction.28Erdős Problem #319 remains OPEN. Statement: What is the size of the largest $A\subseteq\{1, \dots, N\}$ such that there is a function $\delta : A \to \{-1, 1\}$ such that $$ \sum_{n\in A} \frac{\delta n}{n} = 0 $$ and $$ \sum_{n\in A'}\frac{\delta n}{n} \neq 0 $$ for all non-empty $A'\subsetneq A$. Topics: number theory, unit fractions. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: possible.29OBLIGATION (Erdos #319). BANKED: the counting step of the upper bound corroborated numerically. OPEN: the full upper bound is not established by the numerics alone.30Erdős Problem #366 has status 'verifiable'. Statement: Are there any $2$-full $n$ such that $n+1$ is $3$-full? Topics: number theory. Erdős prize: no. Statement is machine-verified in Lean (formal-conjectures). OEIS: A060355.31OBLIGATION (Erdos #366). BANKED: the unconditional Mordell-curve reduction + Pell correction + the two analytic walls verified. OPEN: the analytic walls block an unconditional bound; closing them is open.32

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.