Vela Mathematics Program: problems

Narrowed toformalized ×source:formal-conjectures ×Clear all

Problem ledger

604 problems · 1/13Number SourcesGraph view

declared open · formalized · $500erdos:1

∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), Erdos1.IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N

number theoryadditive combinatoricsA2766612 sources

declared open · formalized · $5000erdos:3

True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k

number theoryadditive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared proved · formalized · $10000erdos:4

True ↔ ∀ C > 0, Erdos4.Erdos4For C

number theoryprimesA0023862 sources

declared proved · formalized · $100erdos:6

{n | primeGap n < primeGap (n + 1) ∧ primeGap (n + 1) < primeGap (n + 2)}.Infinite

number theoryprimesA3352772 sources

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

1 ∈ Erdos9.Erdos9A

number theoryadditive basisprimesA0062862 sources

declared open · formalizederdos:10

True ↔ ∃ k, Erdos10.sumPrimeAndTwoPows k = Set.univ \ {0, 1}

number theoryadditive basisprimesA3870532 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 proved · formalized · $100erdos:13

∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos13.IsForbiddenTripleFree A → ↑A.card ≤ ↑N / 3 + C

number theoryA0022642 sources

declared open · formalizederdos:14

True ↔ ∀ (A : Set ℕ), ∀ ε > 0, Erdos14.almostSquareRoot ε =O[Filter.atTop] Erdos14.nonUniqueSumCount A

number theorysidon setsadditive combinatoricsA143824 · possible2 sources

declared open · formalizederdos:15

True ↔ Summable fun k => (-1) ^ (k + 1) * (↑k + 1) / ↑(Nat.nth Nat.Prime k)

number theoryprimesN/A2 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 open · formalizederdos:17

sorry ↔ {p | Erdos17.IsClusterPrime p}.Infinite

number theoryprimesA0381332 sources

declared open · formalizederdos:18

∀ᶠ (n : ℕ) in Filter.atTop, Erdos18.practicalH n.factorial < n

number theorydivisorsfactorialsA0051532 sources

declared open · formalized · $1000erdos:20

sorry ↔ ∃ c, ∀ (n k : ℕ), n > 0 → Erdos20.f n k < c k ^ n

combinatoricsA3320772 sources

declared proved · formalizederdos:22

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ε * ↑n ∧ ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card

graph theorypossible2 sources

declared falsifiable · formalizederdos:23

∀ (n : ℕ), 0 < n → ∀ H ≤ Erdos23.blowupC5 n, H.IsBipartite → n ^ 2 ≤ ((Erdos23.blowupC5 n).edgeFinset \ H.edgeFinset).card

graph theoryA3896462 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 open · formalized · $500erdos:28

∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

number theoryadditive basisN/A2 sources

declared open · formalized · $1000erdos:30

True ↔ ∀ ε > 0, (fun N => ↑(Erdos30.h N) - √↑N) =O[Filter.atTop] fun N => ↑N ^ ε

number theorysidon setsadditive combinatoricsA143824 · A227590 · A0030222 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 open · formalizederdos:32

True ↔ ∃ A, Erdos32.IsAdditiveComplementToPrimes A ∧ (fun N => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card) =o[Filter.atTop] fun N => Real.log ↑N ^ 2

number theoryadditive basisN/A2 sources

declared open · formalizederdos:33

⨅ A, Filter.limsup (fun N => ↑(↑A ∩ Set.Icc 1 N).ncard / ↑√↑N) Filter.atTop = sorry

number theoryadditive basisN/A2 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 open · formalized · $500erdos:39

True ↔ ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard

number theorysidon setsadditive combinatoricsN/A2 sources

declared open · formalized · $500erdos:40

Erdos40.Erdos40ForSet sorry

number theoryadditive basisN/A2 sources

declared open · formalized · $500erdos:41

∀ (A : Set ℕ), Erdos41.NtupleCondition A 3 → A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

number theorysidon setsadditive combinatoricsN/A2 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:44

True ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card

number theorysidon setsadditive combinatoricsN/A2 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 proved · formalizederdos:48

True ↔ {(n, m) | n.totient = (ArithmeticFunction.sigma 1) m}.Infinite

number theoryN/A2 sources

declared open · formalized · $250erdos:50

sorry ↔ ∀ (f : ℝ → ℝ), Erdos50.IsDistributionOfPhiRatio f → ¬∃ x ∈ Set.Icc 0 1, ∃ y > 0, HasDerivWithinAt f y (Set.Icc 0 1) x

number theoryN/A2 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 open · formalizederdos:60

∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) < G.edgeFinset.card → c * √↑n ≤ ↑{H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard

graph theorycyclesA0068552 sources

declared open · formalizederdos:61

sorry ↔ ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => ↑n ^ c

graph theoryN/A2 sources

declared falsifiable · formalized · $1000erdos:64

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.minDegree ≥ 3 → ∃ k v c, k ≥ 2 ∧ c.IsCycle ∧ c.length = 2 ^ k

graph theorycyclesN/A2 sources

declared open · formalized · $500erdos:66

True ↔ ∃ A c, c ≠ 0 ∧ Filter.Tendsto (fun n => ↑(AdditiveCombinatorics.sumRep A n) / Real.log ↑n) Filter.atTop (nhds c)

number theoryadditive basisN/A2 sources

declared proved · formalized · $500erdos:67

∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|

discrepancyA181740 · A2376952 sources

declared open · formalizederdos:68

True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))

number theoryirrationalityA3313732 sources

declared proved · formalizederdos:69

Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))

number theoryirrationalityA2621532 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science