Vela Mathematics Program: problems

Narrowed toformalized ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

258 problems · 4/6Number SourcesGraph view

declared solved (Lean) · formalizederdos:650

∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊

declared proved (Lean) · formalizederdos:659

True ↔ ∃ A, (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧ (fun n => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)

geometrydistancespossible6 sources

declared disproved (Lean) · formalizederdos:666

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ H ≤ SimpleGraph.hypercube n, ε * ↑n * 2 ^ (n - 1) ≤ ↑H.edgeSet.ncard → (SimpleGraph.cycleGraph 6).IsContained H

graph theorypossible5 sources

declared proved (Lean) · formalizederdos:678

True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, {(m, n) | n + k ≤ m ∧ Finset.lcmInterval m (k + 1) < Finset.lcmInterval n k}.Nonempty

number theorypossible5 sources

declared open · formalizederdos:686

sorry ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

number theoryN/A4 sources

declared open · formalizederdos:689

sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, ∀ m ∈ Finset.Icc 1 n, 2 ≤ {p ∈ Finset.Icc 1 n | Nat.Prime p ∧ a p ≡ m [MOD p]}.card

number theoryN/A3 sources

declared disproved (Lean) · formalizederdos:692

False ↔ ∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∀ (n : ℕ), UnimodularOn (δ n) (n + 1)

number theorydivisorsN/A5 sources

declared solved (Lean) · formalizederdos:694

∀ (fmax fmin : ℕ → ℕ), (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 | ∃ n, ∃ (_ : n ≤ x) (_ : ∃ m, m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)

number theorypossible6 sources

declared proved (Lean) · formalizederdos:698

True ↔ ∃ h, Filter.Tendsto h Filter.atTop Filter.atTop ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → h n ≤ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientspossible5 sources

declared disproved (Lean) · formalized · $1000erdos:707

Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a 1000 dollars prize attached, that every finite Sidon set extends to a perfect difference set modulo

p^2+p+1

for some prime

p

. Alexeev and Mixon establish that

\{1,2,4,8\}

is a counterexample - and discovered along the way that Marshall Hall, Jr. had published a different counterexample three decades before Erdős first posed the problem, unnoticed by the community for half a century.

additive combinatoricssidon setsN/A6 sources

declared proved (Lean) · formalizederdos:728

Whether there are infinitely many integers

a, b, n

with

a, b \ge \varepsilon n

such that

a!\cdot b!

divides

n!\cdot(a+b-n)!

while

a+b

exceeds

n

by more than

C\cdot\log n

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:729

True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite

number theoryfactorialsN/A6 sources

declared open · formalizederdos:730

True ↔ Erdos730.S.Infinite

number theorybinomial coefficientsbase representationsA1295154 sources

declared solved (Lean) · formalizederdos:741

True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

additive combinatoricsN/A6 sources

declared open · formalizederdos:749

True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1

additive combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:750

True ↔ ∀ (f : ℕ → NNReal), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ V G, G.chromaticNumber = ⊤ ∧ ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - f m ≤ ↑I.ncard

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:751

False ↔ ∀ (k : ℕ), ∃ V G, G.chromaticNumber = 4 ∧ ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:753

False ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ), 0 < n → ∀ (G : SimpleGraph (Fin n)), ↑n ^ (1 / 2 + c) < ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ)

graph theorychromatic numberN/A5 sources

declared proved (Lean) · formalizederdos:756

True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)

geometrydistancespossible5 sources

declared proved (Lean) · formalizederdos:760

True ↔ ∃ c > 0, ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ), G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:762

False ↔ ∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V), G.CliqueFree 5 → 4 ≤ G.cochromaticNumber → G.chromaticNumber ≤ G.cochromaticNumber + 2

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:775

False ↔ ∃ C, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, n - C ≤ H.cliqueSizes.ncard

graph theoryhypergraphspossible5 sources

declared proved (Lean) · formalizederdos:785

True ↔ ∀ (A B : Set ℕ), A.Infinite → B.Infinite → Erdos785.IsExactAdditiveComplement A B → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop

additive combinatoricsN/A5 sources

declared disproved (Lean) · formalizederdos:794

False ↔ ∀ (n : ℕ) (H : Finset (Finset (Fin (3 * n)))), H.IsThreeUniform → n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7

graph theoryhypergraphsturan numberN/A5 sources

declared proved (Lean) · formalizederdos:798

True ↔ (fun n => ↑(Erdos798.t n)) =o[Filter.atTop] fun n => ↑n

geometryA1164465 sources

declared proved (Lean) · formalizederdos:818

True ↔ ∀ (K : ℝ), 0 < K → ∃ C, 0 < C ∧ ∃ c, 0 < c ∧ ∀ (A : Finset ℤ), 2 ≤ A.card → ↑(A + A).card ≤ K * ↑A.card → c * ↑A.card ^ 2 / Real.log ↑A.card ^ C ≤ ↑(A * A).card

additive combinatoricsN/A5 sources

declared verifiable · formalizederdos:835

∀ {k : ℕ}, 3 ≤ k → k ≤ 8 → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

graph theoryhypergraphsN/A3 sources

declared proved (Lean) · formalizederdos:844

True ↔ ∀ (N : ℕ), IsGreatest {k | ∃ A ⊆ Finset.Icc 1 N, (∀ a ∈ A, ∀ b ∈ A, ¬Squarefree (a * b)) ∧ A.card = k} (Erdos844.evenOrOddNonSquarefree N).card

number theoryintersecting familyN/A5 sources

declared disproved (Lean) · formalizederdos:845

False ↔ ∀ (C : ℝ), 0 < C → have f := fun x => match x with | (k, l) => 2 ^ k * 3 ^ l; {x | ∃ B, ∃ (h : B.Nonempty) (_ : ↑(B.sup f) ≤ C * ↑(B.inf' h f)), ∑ x ∈ B, f x = x}.HasDensity 0

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:846

False ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A

geometryN/A6 sources

declared decidable · formalizederdos:848

Is the maximum size of a set

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

such that

ab+1

is never squarefree (for all

a,b\in A

) achieved by taking those

n\equiv 7\pmod{25}

? Resolved for all sufficiently large

N

: any near-maximal

A

is contained in

\{n\equiv 7\pmod{25}\}

\{n\equiv 18\pmod{25}\}

, leaving only a finite check.

number theoryN/A4 sources

declared proved · formalizederdos:851

∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d

number theoryN/A4 sources

declared solved (Lean) · formalizederdos:862

False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)

number theorysidon setsA3823955 sources

declared proved (Lean) · formalizederdos:865

∃ C > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

number theoryadditive combinatoricspossible5 sources

declared disproved (Lean) · formalizederdos:867

False ↔ ∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ ↑N / 2 + C

additive combinatoricspossible5 sources

declared solved · formalizederdos:868

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → Filter.Tendsto (fun n => Erdos868.ncard_add_repr A 2 n) Filter.atTop Filter.atTop → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

number theoryadditive basisN/A3 sources

declared disproved (Lean) · formalizederdos:871

False ↔ ∀ (A : Set ℕ), ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧ ∀ (t : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) → ∃ B C, (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧ Disjoint B C ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n

number theoryadditive basisN/A6 sources

declared open · formalizederdos:872

True ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos872.L n) ≥ ε * ↑n

number theoryprimitive setspossible3 sources

declared open · formalizederdos:873

True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)

number theoryN/A3 sources

declared solved · formalizederdos:888

(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

number theorysquaresA3875845 sources

declared disproved (Lean) · formalizederdos:897

False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun x => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) = ⊤ → Filter.limsup (fun n => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

number theoryN/A6 sources

declared proved (Lean) · formalizederdos:898

∀ (A B C P L M N : EuclideanSpace ℝ (Fin 2)), AffineIndependent ℝ ![A, B, C] → P ∈ interior ((convexHull ℝ) {A, B, C}) → N ∈ affineSpan ℝ {A, B} → (affineSpan ℝ {P, N}).direction ⟂ (affineSpan ℝ {A, B}).direction → M ∈ affineSpan ℝ {B, C} → (affineSpan ℝ {P, M}).direction ⟂ (affineSpan ℝ {B, C}).direction → L ∈ affineSpan ℝ {C, A} → (affineSpan ℝ {P, L}).direction ⟂ (affineSpan ℝ {C, A}).direction → dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)

geometryN/A5 sources

declared proved (Lean) · formalizederdos:904

True ↔ ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], ∀ r ∈ Set.Icc 1 (Erdos904.n V), Erdos904.turanNumber (Erdos904.n V) r ≤ G.edgeFinset.card → ∃ s, G.IsNClique r s ∧ 2 * r * G.edgeFinset.card ≤ Erdos904.n V * ∑ v ∈ s, G.degree v

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:905

∀ (n : ℕ) (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], ↑n ^ 2 / 4 < ↑G.edgeFinset.card → ∃ e ∈ G.edgeFinset, ↑n / 6 ≤ ↑(G.trianglesContaining e).card

graph theoryN/A5 sources

declared open · formalizederdos:906

Is there an entire non-zero function

f:\mathbb{C}\to \mathbb{C}

such that, for any infinite sequence

n_1<n_2<\cdots

, the set

\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\}

is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.

analysisiterated functionsN/A5 sources

declared proved (Lean) · formalizederdos:907

True ↔ ∀ (f : ℝ → ℝ), (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) → ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + a

analysisN/A5 sources

declared proved (Lean) · formalizederdos:914

∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], Fintype.card V = r * m → m * (r - 1) ≤ G.minDegree → ∃ K, (∀ (i : Fin m), G.IsNClique r (K i)) ∧ Pairwise fun i j => Disjoint (K i) (K j)

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:923

True ↔ ∀ (V : Type u_1) (n : ℕ), ∃ k, ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3

graph theorychromatic numberN/A5 sources

declared open · formalizederdos:931

sorry ↔ ∀ (k₁ k₂ : ℕ), k₂ ≥ 3 → k₂ ≤ k₁ → {(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite

number theoryN/A3 sources

declared open · formalizederdos:942

Let

h(n)

count powerful integers in

[n^2, (n+1)^2)

. What is the extremal order of

h(n)

number theorypossible4 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science