Problems · Vela Mathematics Program

be infinite with no distinct

A \subset \mathbb{N}

a, b, c \in A

such that

a \mid (b + c)

have positive lower limit? Must every such

b, c > a

. Can

|A \cap [1, N]|/\sqrt{N}

A

fall below

N^{1-c}

infinitely often?

number theoryN/A4 sources

declared disproved (Lean) · formalizederdos:26

be infinite. Must there exist some

A\subset\mathbb{N}

k\geq 1

such that almost all integers have a divisor of the form

a+k

for some

a\in A

? The question as posed follows negatively from Davenport–Erdős (1951). The AI result settles Tenenbaum's harder variant, also negatively: there is an infinite

A

such that for every

k\geq 1

the set of multiples of

A+k

has upper density below

0.34

number theorydivisorsN/A6 sources

declared proved (Lean) · formalizederdos:38

True ↔ ∃ B, ¬B.IsWeakAddBasis ∧ ∃ f, (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧ ∀ (A : Set ℕ) (N : ℕ), have α := schnirelmannDensity A; ∃ b ∈ B, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑N

number theoryN/A6 sources

declared solved (Lean) · formalizederdos:42

True ↔ ∀ M ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}

number theorysidon setsadditive combinatoricsN/A6 sources

declared disproved · formalized · $100erdos:43

If Sidon sets

A, B \subseteq \{1, \dots, N\}

satisfy

(A-A) \cap (B-B) = \{0\}

is the largest Sidon-set size in

\binom{|A|}{2} + \binom{|B|}{2} \le \binom{f(N)}{2} + O(1)

, where

f(N)

[N]

- and can the bound be improved by a fixed proportion when

|A| = |B|

number theorysidon setsadditive combinatoricsA143824 · A227590 · A003022 · possible4 sources

declared disproved (Lean) · formalized · $500erdos:90

Conjectured upper bound on how many pairs among

n

points in the plane can be exactly one unit apart.

geometrydistancesA1867055 sources

declared solved · formalized · $100erdos:119

For unit-modulus complex numbers

z_i

, let

p_n(z)=\prod_{i\le n}(z-z_i)

. Erdős's prize question: is there

M_n=\max_{|z|=1}|p_n(z)|

c>0

\sum_{k\le n} M_k > n^{1+c}

analysispolynomialsN/A4 sources

declared proved (Lean) · formalized · $250erdos:123

be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form

a,b,c>1

a^k b^l c^m

(

k,l,m\ge 0

), none dividing another?

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:125

False ↔ ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity

number theorybase representationsA3670906 sources

declared open · formalizederdos:130

For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.

graph theorychromatic numberN/A4 sources

declared open · formalized · $500erdos:138

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 sources

declared open (Lean) · formalized · $500erdos:146

H

is bipartite and

r

-degenerate, is

\mathrm{ex}(n;H) \ll n^{2-1/r}

(a $500 Erdős-Simonovits prize conjecture)? A counterexample refutes the degeneracy conjecture.

graph theoryturan numberN/A3 sources

declared proved · formalizederdos:152

True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

sidon setsN/A4 sources

declared open (Lean) · formalizederdos:180

For every finite family

\mathcal{F}

of graphs, is there a single

G \in \mathcal{F}

? A counterexample refutes the Erdős-Simonovits compactness conjecture.

\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})

graph theoryturan numberN/A4 sources

declared open (Lean) · formalized · $250erdos:183

-colouring of the edges of

R(3;k)

be the least

n

such that every

k

K_n

contains a monochromatic triangle. Determine

\lim_{k\to\infty} R(3;k)^{1/k}

(a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

graph theoryramsey theoryA0033233 sources

declared solved (Lean) · formalizederdos:202

∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)

covering systemsA3899756 sources

declared disproved (Lean) · formalizederdos:205

False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) n

number theorypossible6 sources

declared open · formalizederdos:254

A \subseteq \mathbb{N}

has unbounded dyadic-shell counts and

\sum_{n \in A} \|\theta n\| = \infty

for every

0 < \theta < 1

be complete - is every sufficiently large integer a sum of distinct elements of

A

A

number theoryN/A4 sources

declared proved (Lean) · formalizederdos:258

True ↔ ∀ (a : ℕ → ℕ), (∀ (n : ℕ), 2 ≤ a n) → Filter.Tendsto a Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 (n + 1), a i))

irrationalityN/A6 sources

declared open · formalizederdos:267

n_1 < n_2 < \cdots

n_{k+1}/n_k \ge c > 1

be irrational? The proposed proof closes the range

\sum_k 1/F_{n_k}

1 < c < 2

left open by earlier criteria.

irrationalityN/A4 sources

declared proved (Lean) · formalizederdos:281

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε

number theorycovering systemsN/A7 sources

declared proved (Lean) · formalizederdos:283

True ↔ ∀ (p : Polynomial ℤ), Erdos283.Condition p

number theoryunit fractionsA3807916 sources

declared open · formalizederdos:306

a/b \in \mathbb{Q}_{>0}

always be written as a finite sum of reciprocals of distinct products of two distinct primes?

b

is squarefree, can

a/b

number theoryunit fractionsN/A4 sources

declared solved · formalizederdos:321

What is the largest

A\subseteq\{1,\dots,N\}

such that all subset sums

\sum_{n\in S}1/n

(over

S\subseteq A

) are distinct?

number theoryunit fractionsA384927 · A3915923 sources

declared open · formalizederdos:326

Does there exist

A=\{a_1<a_2<\cdots\}\subset \mathbb{N}

which is a minimal basis of order

2

(every large integer is the sum of

2

elements from

A

, and no proper subset of

A

has this property) such that

\lim_{k\to \infty}a_k/k^2=c

for some

c\neq 0

? A claimed construction gives a minimal basis with

A(x)=C\sqrt{x}+O(1)

, answering the question affirmatively; Erdős and Graham had conjectured a negative answer.

number theoryadditive basisN/A4 sources

declared proved (Lean) · formalizederdos:330

True ↔ ∃ A h, Erdos330.MinAsymptoticAddBasisOfOrder A h ∧ 0 < A.upperDensity ∧ ∀ n ∈ A, 0 < (Erdos330.UnrepWithout A n h).upperDensity

number theoryadditive basisN/A5 sources

declared disproved (Lean) · formalizederdos:333

False ↔ ∀ (A : Set ℕ), A.HasDensity 0 → ∃ B, A ⊆ B + B ∧ (fun N => ↑(B ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => √↑N

number theoryadditive basisN/A6 sources

declared open · formalizederdos:346

be a set of integers such that

A=\{1\leq a_1< a_2<\cdots\}

A\backslash B

is complete for any finite subset

B

and not complete for any infinite subset

B

. If

a_{n+1}/a_n \geq 1+\epsilon

for all

n

? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2

number theorycomplete sequencesN/A4 sources

declared proved (Lean) · formalizederdos:347

True ↔ ∃ a, Monotone a ∧ Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 2) ∧ ∀ (ι : ℕ → ℕ), (Set.range ι)ᶜ.Finite → (subsetSums (Set.range (a ∘ ι))).HasDensity 1

number theorycomplete sequencesN/A6 sources

declared proved (Lean) · formalizederdos:351

True ↔ ∀ (P : Polynomial ℚ), 0 < P.natDegree → 0 < P.leadingCoeff → Erdos351.HasCompleteImage P

number theorycomplete sequencesN/A6 sources

declared proved (Lean) · formalizederdos:369

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε

number theoryN/A7 sources

declared open · formalizederdos:390

f(n)

be the least

m

for which

n!

can be written as

a_1\cdots a_k

- the smallest possible largest factor in a factorization of

n < a_1 < \cdots < a_k = m

n!

into distinct integers all exceeding

n

. Erdős, Guy and Selfridge proved

f(n) - 2n \asymp n/\log n

. Erdős asked whether there is a constant

c

and what it is. This preprint answers yes and names the constant:

f(n) - 2n \sim c\,\frac{n}{\log n},

\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.

number theoryfactorialsA1934294 sources

declared open · formalizederdos:394

For the least

t_k(n)

, do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with

n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1)

c = 1/2048

admissible in the

t_2

bound.

number theoryA3440054 sources

declared disproved (Lean) · formalizederdos:397

False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite

number theorybinomial coefficientsN/A7 sources

declared proved (Lean) · formalizederdos:401

True ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (r : ℕ), 1 ≤ r → {n | ∃ a₁ a₂, 0 < a₁ ∧ 0 < a₂ ∧ ↑a₁ + ↑a₂ > ↑n + f r * Real.log ↑n ∧ a₁.factorial * a₂.factorial ∣ n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite

number theoryfactorialsN/A6 sources

declared open · formalizederdos:424

a_1 = 2

and continue the sequence by appending to

a_2 = 3

a_1, \dots, a_n

all possible values of

a_ia_j - 1

. Is it true that the set of integers which eventually appear has positive density?

i \ne j

number theoryA0052444 sources

declared open · formalizederdos:450

How large must

y(\varepsilon, n)

be so that every interval

(x, x+y)

contains at most

\varepsilon y

integers having a divisor in

(n, 2n)

? The candidate proof gives the sharp fixed-

\varepsilon

order

y = \Theta_\varepsilon(n)

, uniformly in the translate.

number theorydivisorsN/A4 sources

declared proved (Lean) · formalizederdos:457

True ↔ ∃ ε > 0, {n | ∀ (p : ℕ), ↑p ≤ (2 + ε) * Real.log ↑n → Nat.Prime p → p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log ↑n⌋₊, (n + i)}.Infinite

number theoryA3916686 sources

declared proved (Lean) · formalizederdos:469

Does the sum of the reciprocals of all primitive pseudoperfect numbers converge?

number theorydivisorsA006036 · A119425 · possible5 sources

declared open · formalizederdos:477

Does there exist an integer polynomial

f

of degree at least two and a set

A \subseteq \mathbb{Z}

such that every integer has a unique representation

n = a + f(k)

? A manuscript claims the thirteenth powers admit a tiling complement.

number theoryN/A4 sources

declared open · formalizederdos:489

A

is a forbidden-divisor set with

|A \cap [1,x]| = o(\sqrt{x})

converge to a finite limit?

B = \{b_1 < b_2 < \cdots\}

the sifted set, must

x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2

number theoryN/A4 sources

declared open · formalizederdos:501

For every

x \in \mathbb{R}

let

A_x \subset \mathbb{R}

be a bounded set of Lebesgue outer measure

< 1

. Must there be an infinite independent set, that is an infinite

X \subseteq \mathbb{R}

? Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal. The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

x \notin A_y

for all distinct

x, y \in X

combinatoricsset theoryN/A4 sources

declared open · formalizederdos:522

For

P_n(z) = \sum_{k=0}^n \varepsilon_k z^k

with independent uniform signs, does the number

R_n

of roots in

|z| \le 1

satisfy

R_n/(n/2) \to 1

almost surely? The manuscript proves the strong law with

R_n = n/2 + O_\omega(n^{149/150})

analysispolynomialsprobabilityN/A4 sources

declared open · formalizederdos:538

If each integer has at most

r

representations

m = pa

, what is the best upper bound for

p

prime and

a \in A \subseteq [1, N]

\sum_{a \in A} 1/a

? The candidate proof gives the matching order

\Theta_r(\log N / \log\log N)

number theoryN/A5 sources

declared open · formalizederdos:539

For

|A| = n

, how small can the cofactor set

Q(A) = \{a / \gcd(a,b) : a, b \in A\}

be? The answer is

h(n) = n^{1/2 + o(1)}

: a new upper bound

h(n) \le n^{1/2} \exp(O(\sqrt{\log n}))

matches the classical lower bound.

number theorypossible5 sources

declared open · formalized · $500erdos:593

Which finite triple systems occur in every triple system of uncountable chromatic number? The claimed characterization: exactly those that, after removing isolated vertices, are linear, have every hyperedge-node of their Levi graph meeting a bridge, and have every Berge cycle even.

set theorygraph theoryhypergraphsN/A4 sources

declared solved (Lean) · formalizederdos:619

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)

graph theoryN/A5 sources

declared open · formalizederdos:623

X

be a set of cardinality

\aleph_\omega