Vela Mathematics Program: problems

Problem ledger

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 openerdos:148

Erdős problem 148

number theoryunit fractionsA076393 · A006585

declared disproved (Lean) · formalizederdos:206

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

number theoryunit fractionsN/A5 sources

declared falsifiable · formalizederdos:242

∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

number theoryunit fractionsA073101 · A075245 · A075246 · A075247 · A075248 · A2871162 sources

declared open · formalizederdos:282

∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0

number theoryunit fractionsN/A2 sources

declared proved (Lean) · formalizederdos:283

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

number theoryunit fractionsA3807916 sources

declared provederdos:284

Erdős problem 284

number theoryunit fractionspossible

declared proved · formalizederdos:285

True ↔ ∀ (f : ℕ → ℕ) (S : Set ℕ), S = {k | ∃ n, StrictMono n ∧ 0 ∉ Set.range n ∧ 1 = ∑ i, 1 / ↑(n i)} → (∀ k ∈ S, IsLeast {x | ∃ n, ∃ (_ : StrictMono n) (_ : 0 ∉ Set.range n) (_ : 1 = ∑ i, 1 / ↑(n i)), n (Fin.last k) = x} (f k)) → ∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ k ∈ S, ↑(f k) = (1 + o k) * Real.exp 1 / (Real.exp 1 - 1) * (↑k + 1)

number theoryunit fractionsA0306592 sources

declared provederdos:286

Erdős problem 286

number theoryunit fractionsN/A

declared falsifiable · formalizederdos:287

True ↔ ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i, 1 / ↑(s i) = 1 → 3 ≤ Erdos287.max_gap k s

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:288

sorry ↔ {I | ∀ (j : Fin 2), (I j).1 ≤ (I j).2 ∧ ∃ n, ∑ j, ∑ nⱼ ∈ (Set.Icc (I j).1 (I j).2).toFinset, (↑↑nⱼ)⁻¹ = ↑↑n}.Finite

number theoryunit fractionsN/A3 sources

declared open · formalizederdos:289

True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, ∃ I, (∀ (i : Fin k), (I i).1 < (I i).2) ∧ (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧ ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1

number theoryunit fractionsN/A2 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 provederdos:292

Erdős problem 292

number theoryunit fractionsA092671

declared openerdos:293

Erdős problem 293

number theoryunit fractionspossible

declared provederdos:294

Erdős problem 294

number theoryunit fractionspossible

declared open · formalizederdos:295

sorry ↔ Filter.Tendsto (fun N => ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTop

number theoryunit fractionsA1928812 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

declared solvederdos:297

Erdős problem 297

number theoryunit fractionsA092670

declared proved (Lean) · formalizederdos:298

True ↔ ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity → ∃ S, ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

number theoryunit fractionsN/A4 sources

declared disproved (Lean) · formalizederdos:299

False ↔ ∃ a, StrictMono a ∧ (∀ (n : ℕ), 0 < a n) ∧ (fun n => ↑(a (n + 1)) - ↑(a n)) =O[Filter.atTop] 1 ∧ ∀ (S : Finset ℕ), ∑ i ∈ S, 1 / ↑(a i) ≠ 1

number theoryunit fractionsN/A4 sources

declared solvederdos:300

Erdős problem 300

number theoryunit fractionsA390393

declared openerdos:301

Erdős problem 301

number theoryunit fractionsA390394

declared open · formalizederdos:302

∀ (f : ℕ → ℕ), (∀ (N : ℕ), Erdos302.IsMaxNoTripleCard N (f N)) → Filter.Tendsto (fun N => ↑(f N) / ↑N) Filter.atTop (nhds sorry)

number theoryunit fractionsA3903953 sources

declared proved (Lean) · formalizederdos:303

True ↔ ∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite → ∃ a b c, [a, b, c, 0].Nodup ∧ 1 / ↑a = 1 / ↑b + 1 / ↑c ∧ (𝓒 '' {a, b, c}).Subsingleton

number theoryunit fractionsN/A5 sources

declared open · formalizederdos:304

∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → a ∣ b

number theoryunit fractionsA097847 · A0978492 sources

declared provederdos:305

Erdős problem 305

number theoryunit fractionspossible

declared open · formalizederdos:306

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

and

b

is squarefree, can

a/b

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

number theoryunit fractionsN/A4 sources

declared verifiable · formalizederdos:307

sorry ↔ ∃ P Q, (∀ p ∈ P, Nat.Prime p) ∧ (∀ q ∈ Q, Nat.Prime q) ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹

number theoryunit fractionsN/A2 sources

declared provederdos:308

Erdős problem 308

number theoryunit fractionspossible

declared disprovederdos:309

Erdős problem 309

number theoryunit fractionsA217693

declared provederdos:310

Erdős problem 310

number theoryunit fractionsN/A

declared openerdos:311

Erdős problem 311

number theoryunit fractionsN/A

declared open · formalizederdos:312

True ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:313

sorry ↔ Erdos313.erdos313Solutions.Infinite

number theoryunit fractionsA0543772 sources

declared proved (Lean) · formalizederdos:314

True ↔ Filter.liminf (fun n => ↑n ^ 2 * Erdos314.epsilon n) Filter.atTop = 0

number theoryunit fractionsN/A5 sources

declared proved (Lean) · formalizederdos:315

True ↔ ∀ (a : ℕ → ℕ), (∀ (i : ℕ), 0 < a i) → StrictMono a → (∃ i, a i ≠ Erdos315.u i + 1) → ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c₀

number theoryunit fractionsA000058 · A0763935 sources

declared disproved (Lean) · formalizederdos:316

False ↔ ∀ (A : Finset ℕ), 0 ∉ A → 1 ∉ A → ∑ n ∈ A, 1 / ↑n < 2 → ∃ A₁ A₂, Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧ ∑ n ∈ A₁, 1 / ↑n < 1 ∧ ∑ n ∈ A₂, 1 / ↑n < 1

number theoryunit fractionsN/A4 sources

declared open · formalizederdos:317

∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)

number theoryunit fractionsN/A2 sources

declared solved · formalizederdos:318

∃ A, A.HasPosDensity ∧ ¬Erdos318.P₁ A

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:319

∀ (N : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A ⊆ Finset.Icc 1 N) (_ : ∃ δ, ∑ n ∈ A, ↑↑(δ n) / ↑n = 0 ∧ ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', ↑↑(δ n) / ↑n ≠ 0), A.card = x} sorry

number theoryunit fractionspossible2 sources

declared solvederdos:320

Let

S(N)

count the distinct values of

\sum_{n\in A} 1/n

over

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

. Estimate

S(N)

number theoryunit fractionsA0722072 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 openerdos:327

Erdős problem 327

number theoryunit fractionsA3849272 sources

declared proved (Lean) · formalizederdos:355

True ↔ ∃ A, IsLacunary A ∧ ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}

number theoryunit fractionsN/A5 sources

Problems · Vela Mathematics Program

Problem ledger