Vela Mathematics Program: problems

Narrowed tosource:plby-lean-proofs ×Clear all

Problem ledger

196 problems · 1/4Number SourcesGraph view

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 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 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 proved (Lean) · formalizederdos:45

True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1

number theoryunit fractionsramsey theorypossible4 sources

declared proved (Lean) · formalizederdos:46

True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).Subsingleton

number theoryunit fractionsramsey theoryN/A4 sources

declared proved (Lean) · formalized · $100erdos:47

True ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, δ * Real.log ↑N < A.reciprocalSum → ∃ S ⊆ A, S.reciprocalSum = 1

number theoryunit fractionsN/A4 sources

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

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

number theoryintersecting familyN/A5 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 solved · formalized · $100erdos:119

For unit-modulus complex numbers

z_i

, let

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

and

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

. Erdős's prize question: is there

c>0

with

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

analysispolynomialsN/A4 sources

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

Let

a,b,c>1

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

a^k b^l c^m

(

k,l,m\ge 0

), none dividing another?

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

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

graph theorypossible5 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 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 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 proved (Lean)erdos:237

Erdős problem 237

number theoryprimesN/A4 sources

declared proved (Lean) · formalizederdos:246

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

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

Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.moebius n) ^ 2 * ↑n / 2 ^ n)

irrationalityA3711345 sources

declared open · formalizederdos:264

¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x

irrationalityN/A4 sources

declared proved (Lean) · formalizederdos:268

∀ (d : ℕ), (interior {x | ∃ A, A.Infinite ∧ (Summable fun n => 1 / ↑↑n) ∧ x = fun i => ∑' (n : ↑A), 1 / (↑↑n + ↑↑i)}).Nonempty

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:275

∀ (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ), (∃ k, ∀ x ∈ Set.Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD ↑(n i)]) → ∀ (x : ℤ), ∃ i, x ≡ a i [ZMOD ↑(n i)]

number theorycovering systemsN/A5 sources

declared disproved (Lean) · formalizederdos:280

False ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)

number theorycovering systemsN/A5 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 proved (Lean) · formalizederdos:290

True ↔ ∀ (a : ℕ), 1 ≤ a → ∃ b, a < b ∧ Erdos290.harmonicDen a (b + 1) < Erdos290.harmonicDen a b

number theoryunit fractionsA3750815 sources

declared open · formalizederdos:291

Erdos291.L 1 = 1 ∧ Erdos291.L 2 = 2 ∧ Erdos291.L 3 = 6 ∧ Erdos291.L 4 = 12

number theoryunit fractionsA1105663 sources

declared proved (Lean) · formalizederdos:296

(∀ (N k : ℕ), Erdos296.HasDisjointUnitDecomps N k → ↑k ≤ Erdos296.recipSum (Finset.Icc 1 N)) ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ᶠ (N : ℕ) in Filter.atTop, Erdos296.HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log ↑N⌋₊

number theoryunit fractionspossible5 sources

Problems · Vela Mathematics Program

Problem ledger