Results for depends.

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.

Erdős Problem #700 remains OPEN. Topics: number theory, binomial coefficients. Erdős prize: no. Not yet formalized in Lean. OEIS: A091963, possible.

Erdő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.

Erdő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.

Erdős Problem #993 has status 'falsifiable'. Topics: graph theory. Erdős prize: no. Not yet formalized in Lean. OEIS: possible.

Erdő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.

Erdő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.

Erdő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.

Erdő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.

Erdő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.

Erdő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.

Erdő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.

Erdős Problem #684 remains OPEN. Topics: number theory, primes, binomial coefficients. Erdős prize: no. Not yet formalized in Lean. OEIS: A392019, possible.

Erdő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.

Erdő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.

Erdő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.

BENCHMARK CLAIM (ProteinGym) — ESM-1v REPORTS strong zero-shot substitution performance from masked-marginal scoring of a protein language model. VERIFICATION STATE: author-reported; weights public; depends on the scoring convention (masked-marginal vs wt-marginal) and the ProteinGym version. NOT re-run here. Open obligation: re-score the released model on the pinned v1.1 zero-shot substitution set.

BENCHMARK CLAIM (MiniF2F) — Draft-Sketch-Prove (DSP) REPORTS improved miniF2F-test pass by drafting an informal proof, sketching a formal skeleton, then closing gaps with an ATP. VERIFICATION STATE: author-reported; pipeline described; depends on the underlying ATP and the autoformalizer, both of which drift. NOT re-run here. Open obligation: reproduce with pinned ATP + LLM versions.

BENCHMARK CLAIM (ProteinGym) — ProteinNPT (non-parametric transformer, supervised track) REPORTS gains by attending across labelled neighbours. VERIFICATION STATE: author-reported; SUPERVISED — not comparable to zero-shot numbers; depends on the cross-validation split. NOT re-run here. Open obligation: re-run under the official supervised CV split; never compare against zero-shot rows.