Vela Mathematics Program: problems

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

Problem ledger

258 problems · 1/6Number SourcesGraph view

declared verifiable · formalizederdos:7

Can there be a finite covering system of the integers with distinct moduli, all of which are odd and greater than

1

number theorycovering systemsN/A4 sources

declared open · formalizederdos:11

∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ l

number theoryadditive basisA001220 · A3775873 sources

declared open · formalizederdos:12

Let

A \subset \mathbb{N}

be infinite with no distinct

a, b, c \in A

such that

a \mid (b + c)

with

b, c > a

. Can

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

have positive lower limit? Must every such

A

fall below

N^{1-c}

infinitely often?

number theoryN/A4 sources

declared disproved (Lean) · formalizederdos:16

False ↔ ∃ A B, Erdos16.Erdos16Set = A ∪ B ∧ (∃ a, ∃ d > 0, A = {x | ∃ m, x = a + m * d}) ∧ Erdos16.density_zero B

number theoryadditive basisprimesA0062855 sources

declared proved (Lean) · formalizederdos:24

True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin (5 * n))), G.CliqueFree 3 → G.copyCount (SimpleGraph.cycleGraph 5) ≤ n ^ 5

graph theorypossible5 sources

declared open · formalizederdos:25

True ↔ ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ (i : ℕ), 0 < seq_n i) → StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d

number theoryN/A3 sources

declared disproved (Lean) · formalizederdos:26

Let

A\subset\mathbb{N}

be infinite. Must there exist some

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:31

∀ (A : Set ℕ), A.Infinite → ∃ B, B.HasDensity 0 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, n ∈ A + B

number theoryadditive basisN/A5 sources

declared disproved (Lean) · formalizederdos:34

False ↔ ∀ (c : ℝ), 0 < c → ∃ N, ∀ n ≥ N, ∀ (p : Equiv.Perm (Fin n)), ↑(Erdos34.consecutiveSums n p).card < c * ↑n ^ 2

number theoryA389241 · A234813 · A3901875 sources

declared open · formalizederdos:36

Erdos36.M 5 = 3

number theoryadditive combinatoricsA393584 · possible3 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\}

, must

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

, where

f(N)

is the largest Sidon-set size in

[N]

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

|A| = |B|

number theorysidon setsadditive combinatoricsA143824 · A227590 · A003022 · possible4 sources

declared open · formalizederdos:51

True ↔ ∃ A n, A.Infinite ∧ (∀ (a : ↑A), IsLeast (Nat.totient ⁻¹' {↑a}) (n a)) ∧ Filter.Tendsto (fun a => ↑(n a) / ↑↑a) Filter.atTop Filter.atTop

number theoryA002202 · A0141973 sources

declared open · formalized · $250erdos:52

True ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ C, 0 < C ∧ ∀ (A : Finset ℤ), max ↑(A + A).card ↑(A * A).card ≥ C * ↑A.card ^ (2 - ε)

number theoryadditive combinatoricsA2639963 sources

declared disproved (Lean) · formalized · $10erdos:56

∀ {A : Finset ℕ}, Erdos56.WeaklyDivisible 0 A ↔ A = ∅

number theoryintersecting familyN/A5 sources

declared proved (Lean) · formalizederdos:71

True ↔ ∀ (P : Set ℕ), P.IsAPOfLength ⊤ → (∃ n ∈ P, Even n) → ∃ c, ∀ (V : Type) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], c ≤ G.averageDegree → ∃ v w, w.IsCycle ∧ w.length ∈ P

graph theorycyclesN/A4 sources

declared open · formalizederdos:75

True ↔ ∃ V G, G.chromaticCardinal = Cardinal.aleph 1 ∧ Cardinal.mk V = Cardinal.aleph 1 ∧ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph), H.verts.ncard = n → ∃ I, ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)

graph theorychromatic numberN/A3 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 proved (Lean) · formalizederdos:93

∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

geometryconvexdistancesN/A5 sources

declared proved (Lean) · formalized · £25erdos:94

∃ C > 0, ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑P → ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3

geometryconvexdistancesA3878585 sources

declared disproved (Lean) · formalized · $50erdos:105

False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}

geometryN/A5 sources

declared proved (Lean) · formalizederdos:115

True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2

polynomialsanalysisN/A5 sources

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared open · formalizederdos:124

∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹

number theorybase representationsN/A4 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 proved (Lean) · formalizederdos:134

True ↔ ∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∃ N, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 3 → (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) → ∃ H, G ≤ H ∧ H.CliqueFree 3 ∧ (∀ (x y : Fin n), x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.Adj z y) ∧ ↑(H.edgeFinset \ G.edgeFinset).card ≤ δ * ↑n ^ 2

graph theoryN/A5 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 proved (Lean) · formalizederdos:150

True ↔ ∃ α < 2, Filter.Tendsto (fun n => ↑(Erdos150.maxMinimalCuts n) ^ (1 / ↑n)) Filter.atTop (nhds α)

graph theorypossible5 sources

declared proved · formalizederdos:152

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

sidon setsN/A4 sources

declared proved (Lean) · formalizederdos:154

True ↔ ∀ (m : ℕ), 2 ≤ m → ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop → (∀ (k x : ℕ), x ∈ A k → x ≤ N k) → (∀ (k : ℕ), IsSidon ↑(A k)) → Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) → ∀ i < m, Filter.Tendsto (fun k => ↑{s ∈ A k + A k | s % m = i}.card / ↑(A k + A k).card) Filter.atTop (nhds (1 / ↑m))

sidon setsN/A6 sources

declared proved (Lean) · formalizederdos:164

True ↔ ∀ (A : Set ℕ), (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)

number theoryprimitive setsA1372455 sources

declared proved (Lean) · formalizederdos:178

True ↔ ∀ (a : ℕ → ℕ → ℕ), (∀ (i : ℕ), StrictMono (a i)) → ∃ f, (∀ (n : ℕ), f n = 1 ∨ f n = -1) ∧ ∀ (d : ℕ), ∃ C, ∀ (m i : ℕ), i < d → |∑ j ∈ Finset.range m, f (a i j)| ≤ ↑C

discrepancyN/A5 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared disproved (Lean) · formalizederdos:194

False ↔ ∀ k ≥ 3, ∀ (r : ℝ → ℝ → Prop), IsStrictTotalOrder ℝ r → ∃ s, s.IsAPOfLength k ∧ (List.Pairwise r s ∨ List.Pairwise (flip r) s)

arithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:198

∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2

additive combinatoricssidon setsarithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:199

False ↔ ∀ (A : Set ℝ), ThreeAPFree A → ∃ S, S.IsAPOfLength ⊤ ∧ S ⊆ Aᶜ

arithmetic progressionsN/A5 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:204

False ↔ ∃ n a, have D := {d | d ∣ n ∧ d > 1}; (∀ (x : ℤ), ∃ d ∈ D, x ≡ a d [ZMOD ↑d]) ∧ ∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x, x ≡ a d [ZMOD ↑d] ∧ x ≡ a d' [ZMOD ↑d']) → d.gcd d' = 1

covering systemsN/A5 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 disproved (Lean) · formalizederdos:206

False ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), Erdos206.EventuallyGreedy x

number theoryunit fractionsN/A5 sources

declared disproved (Lean) · formalizederdos:209

False ↔ ∀ (d : ℕ), 4 ≤ d → ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))), A.card = d → (∀ L ∈ A, Erdos209.IsLine L) → ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) → (∀ (p : EuclideanSpace ℝ (Fin 2)), Erdos209.pointMultiplicity A p ≤ 3) → Erdos209.HasGallaiTriangle A

geometryN/A4 sources

declared proved (Lean) · formalizederdos:214

True ↔ ∀ (S : Set (EuclideanSpace ℝ (Fin 2))), Erdos214.UnitDistanceAvoiding S → ∃ p, (∀ (i : Fin 4), p i ∈ Sᶜ) ∧ Congruent p Erdos214.unitSquare

geometrydistancesN/A5 sources

declared open · formalizederdos:218

{n | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

number theoryprimesA333230 · A333231 · A0641133 sources

declared proved (Lean) · formalizederdos:221

True ↔ ∃ A, ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a

number theoryadditive basisN/A5 sources

declared proved (Lean) · formalizederdos:224

∀ {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))), A.card = 2 ^ d + 1 → ∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ Erdos224.ObtuseAt x y z

geometryN/A5 sources

declared proved (Lean) · formalizederdos:226

True ↔ ∃ F, Differentiable ℂ F ∧ (∀ (x : ℝ), (F ↑x).im = 0) ∧ (∀ (g : ℝ →ᵃ[ℝ] ℝ), (fun x => (F ↑x).re) ≠ ⇑g) ∧ Erdos226.PreservesRationality fun x => (F ↑x).re

analysisN/A5 sources

declared proved (Lean) · formalizederdos:229

True ↔ ∀ (S : ℕ → Set ℂ), (∀ (n : ℕ), derivedSet (S n) = ∅) → ∃ f, Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f ∧ ∀ n ≥ 1, ∃ k, ∀ z ∈ S n, iteratedDeriv k f z = 0

analysisiterated functionsN/A5 sources

declared open · formalizederdos:233

(fun N => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ 2

number theoryprimesA0747413 sources

declared proved (Lean) · formalizederdos:246

∀ (a b : ℕ), 2 ≤ a → 2 ≤ b → a.Coprime b → IsAddComplete (Erdos246.Gamma a b)

number theoryN/A5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science