Vela Mathematics Program: problems

Problem ledger

1,217 problems · 17/25Number SourcesGraph view

declared provederdos:801

Erdős problem 801

graph theoryramsey theoryN/A

declared openerdos:802

Erdős problem 802

graph theoryN/A

declared disprovederdos:803

Erdős problem 803

graph theoryN/A

declared disprovederdos:804

Erdős problem 804

graph theorypossible

declared openerdos:805

Erdős problem 805

graph theorypossible

declared provederdos:806

Erdős problem 806

additive combinatoricspossible

declared disprovederdos:807

Erdős problem 807

graph theoryN/A

declared disprovederdos:808

Erdős problem 808

additive combinatoricsgraph theoryN/A

declared openerdos:809

Erdős problem 809

graph theoryramsey theorypossible

declared openerdos:810

Erdős problem 810

graph theoryramsey theorypossible

declared openerdos:811

Erdős problem 811

graph theoryramsey theorypossible

declared open · formalizederdos:812

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + c

graph theoryramsey theoryA0594422 sources

declared openerdos:813

Erdős problem 813

graph theorypossible

declared provederdos:814

Erdős problem 814

graph theorypossible

declared disprovederdos:815

Erdős problem 815

graph theoryN/A

declared provederdos:816

Erdős problem 816

graph theoryN/A

declared open · formalizederdos:817

True ↔ (fun n => 3 ^ n) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)

additive combinatoricspossible2 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 openerdos:819

Erdős problem 819

additive combinatoricspossible2 sources

declared openerdos:820

Erdős problem 820

number theoryA263647

declared open · formalizederdos:821

True ↔ ∀ ε > 0, {n | ↑(Erdos821.g n) > ↑n ^ (1 - ε)}.Infinite

number theoryA0141972 sources

declared proved · formalizederdos:822

True ↔ (Set.range fun n => n + n.totient).HasPosDensity

number theoryA121048 · A1550852 sources

declared provederdos:823

Erdős problem 823

number theoryN/A

declared openerdos:824

Erdős problem 824

number theorypossible

declared proved · formalized · $25erdos:825

True ↔ ∃ C, ∃ (_ : C > 0), ∀ (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) > C * ↑n → ∃ s ⊆ n.properDivisors, n = s.sum id

number theoryA006037 · A3302442 sources

declared open · formalizederdos:826

True ↔ ∃ C > 0, {n | ∀ k ≥ 1, ↑((ArithmeticFunction.sigma 0) (n + k)) ≤ C * ↑k}.Infinite

number theoryN/A2 sources

declared openerdos:827

Erdős problem 827

geometrypossible

declared open · formalizederdos:828

True ↔ ∀ (a : ℤ), {n | ↑n.totient ∣ ↑n + a}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:829

True ↔ ∃ C, (fun n => ↑(AdditiveCombinatorics.sumRep Erdos829.cubes n)) =O[Filter.atTop] fun n => Real.log ↑n ^ C

number theorypossible2 sources

declared open · formalizederdos:830

sorry ↔ {(a, b) | IsAmicable a b}.Infinite

number theoryA2591802 sources

declared openerdos:831

Erdős problem 831

geometrypossible

declared disprovederdos:832

Erdős problem 832

graph theoryhypergraphschromatic numberpossible

declared provederdos:833

Erdős problem 833

graph theoryhypergraphschromatic numberpossible

declared solvederdos:834

Erdős problem 834

graph theoryhypergraphsN/A

declared verifiable · formalizederdos:835

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

graph theoryhypergraphsN/A3 sources

declared openerdos:836

Erdős problem 836

graph theoryhypergraphschromatic numberN/A2 sources

declared openerdos:837

Erdős problem 837

graph theoryhypergraphsN/A

declared openerdos:838

Erdős problem 838

geometryconvexpossible

declared openerdos:839

Erdős problem 839

number theoryN/A

declared openerdos:840

Erdős problem 840

additive combinatoricssidon setsN/A

declared solvederdos:841

Erdős problem 841

number theoryA092487

declared provederdos:842

Erdős problem 842

graph theorychromatic numberN/A

declared provederdos:843

Erdős problem 843

number theoryN/A

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 disproved · formalizederdos:847

False ↔ ∀ (A : Set ℕ), Infinite ↑A → Erdos847.HasFew3APs A → ∃ n S, (∀ (i : Fin n), ThreeAPFree (S i)) ∧ A = ⋃ i, S i

additive combinatoricsN/A3 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 open · formalizederdos:849

True ↔ ∀ t ≥ 1, ∃ a, {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard = t

number theorybinomial coefficientsA003016 · A003015 · A059233 · A098565 · A090162 · A180058 · A1822372 sources

declared open · formalizederdos:850

True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors

number theoryprimesA3431013 sources

Problems · Vela Mathematics Program

Problem ledger