Vela Mathematics Program: problems

Narrowed tosource:erdos-ai-contributions-wiki ×Clear all

Problem ledger

353 problems · 3/8Number SourcesGraph view

declared proved (Lean) · formalizederdos:379

Filter.limsup (fun n => ↑(Erdos379.S n)) Filter.atTop = ⊤

number theorybinomial coefficientspossible5 sources

declared provederdos:380

Erdős problem 380

number theoryA070003 · A388654 · A387054 · A3891003 sources

declared openerdos:388

Erdős problem 388

number theoryN/A2 sources

declared open · formalizederdos:390

Let

f(n)

be the least

m

for which

n!

can be written as

a_1\cdots a_k

with

n < a_1 < \cdots < a_k = m

- the smallest possible largest factor in a factorization of

n!

into distinct integers all exceeding

n

. Erdős, Guy and Selfridge proved

f(n) - 2n \asymp n/\log n

. Erdős asked whether there is a constant

c

with

f(n) - 2n \sim c\,\frac{n}{\log n},

and what it is. This preprint answers yes and names the constant:

\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.

number theoryfactorialsA1934294 sources

declared proved (Lean) · formalizederdos:392

∀ (A : ℕ → ℕ), (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) → (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

number theoryfactorialspossible5 sources

declared openerdos:393

Erdős problem 393

number theoryfactorialsA3883022 sources

declared open · formalizederdos:396

True ↔ ∀ (k : ℕ), ∃ n, n.descFactorial (k + 1) ∣ n.centralBinom

number theorybinomial coefficientsA3750773 sources

declared disproved (Lean) · formalizederdos:397

False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite

number theorybinomial coefficientsN/A7 sources

declared disproved (Lean) · formalizederdos:399

False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

number theoryfactorialsN/A5 sources

declared open · formalizederdos:400

True ↔ ∀ k ≥ 2, ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x => c * ↑x * Real.log ↑x

number theoryfactorialspossible3 sources

declared proved (Lean) · formalizederdos:401

True ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (r : ℕ), 1 ≤ r → {n | ∃ a₁ a₂, 0 < a₁ ∧ 0 < a₂ ∧ ↑a₁ + ↑a₂ > ↑n + f r * Real.log ↑n ∧ a₁.factorial * a₂.factorial ∣ n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:403

True ↔ {p | (∀ a ∈ p.2, 0 < a) ∧ 2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite

number theoryfactorialsN/A4 sources

declared openerdos:411

Erdős problem 411

number theoryiterated functionsA383044 · possible2 sources

declared openerdos:415

Erdős problem 415

number theorypossible2 sources

declared proved (Lean) · formalizederdos:418

True ↔ {x | ∃ n, n - n.totient = x}ᶜ.Infinite

number theoryA005278 · A2639585 sources

declared solved (Lean) · formalizederdos:419

{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet

number theoryfactorialsN/A5 sources

declared openerdos:423

Erdős problem 423

number theoryA0052432 sources

declared openerdos:425

Erdős problem 425

number theorysidon setspossible2 sources

declared disproved (Lean) · formalized · $25erdos:426

False ↔ ∃ c, 0 < c ∧ ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, c * (2 ^ n.choose 2 / ↑n.factorial) ≤ ↑H.uniqueSubgraphCount

graph theorypossible5 sources

declared proved (Lean) · formalizederdos:427

True ↔ Erdos427.erdos427

number theoryprimesN/A5 sources

declared disproved (Lean) · formalizederdos:429

False ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (A : Set ℕ), A.Infinite → (∀ (N : ℕ), (A ∩ Set.Icc 1 N).ncard ≤ f N) → (∀ (p : ℕ), Nat.Prime p → ∃ b, ∀ a ∈ A, ↑a ≠ b) → ∃ n, ∀ a ∈ A, Nat.Prime (n + a)

number theoryN/A5 sources

declared openerdos:432

Erdős problem 432

number theoryN/A2 sources

declared proved (Lean)erdos:433

Erdős problem 433

number theorypossible4 sources

declared proved (Lean) · formalizederdos:434

∀ (n k : ℕ), 1 ≤ n → 2 ≤ k → k ≤ n → IsGreatest {x | ∃ S, ∃ (_ : S ⊆ Finset.Icc 1 n) (_ : S.card = k) (_ : S.gcd id = 1), Erdos434.Nat.NcardUnrepresentable ↑S = x} (Erdos434.Nat.NcardUnrepresentable (Set.Icc (n - k + 1) n))

number theorypossible5 sources

declared proved (Lean) · formalizederdos:435

∀ (n : ℕ), n ≠ 0 → (∀ (p k : ℕ), Nat.Prime p → n ≠ p ^ k) → IsGreatest {m | ¬∃ c, m = ∑ i ∈ Finset.Ico 1 n, ↑(c i) * ↑(n.choose i)} (∑ p ∈ n.primeFactors, (∑ d ∈ Finset.Icc 1 (n.factorization p), ↑(n.choose (p ^ d))) * (↑p - 1) - ↑n)

number theoryA3894795 sources

declared disprovederdos:441

Erdős problem 441

number theoryA0685092 sources

declared proved (Lean) · formalizederdos:443

True ↔ ∀ (s : ℕ), ∃ m, ∃ n < m, s ≤ (Erdos443.A n ∩ Erdos443.A m).card

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:447

True ↔ (fun n => ↑(Erdos447.maxUnionFree n)) =o[Filter.atTop] fun n => 2 ^ n

combinatoricspossible5 sources

declared openerdos:451

Let

n_k

be the least integer greater than

2k

for which

\prod_{i=1}^k (n_k - i)

has no prime factor in

(k, 2k)

. How rapidly must

n_k

grow?

number theoryA3866203 sources

declared disproved (Lean) · formalizederdos:453

False ↔ Erdos453.EventuallyHasPrimeWitness

number theoryN/A5 sources

declared open · formalizederdos:456

True ↔ Filter.Tendsto (fun N => ↑(Nat.count {n | Erdos456.m n < Erdos456.p n} N) / ↑N) Filter.atTop (nhds 1)

number theoryA034694 · A061026 · possible3 sources

declared proved (Lean) · formalizederdos:457

True ↔ ∃ ε > 0, {n | ∀ (p : ℕ), ↑p ≤ (2 + ε) * Real.log ↑n → Nat.Prime p → p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log ↑n⌋₊, (n + i)}.Infinite

number theoryA3916686 sources

declared solved (Lean) · formalizederdos:459

∀ {u : ℕ}, 2 ≤ u → u + 2 ≤ Erdos459.f u ∧ Erdos459.f u ≤ u ^ 2

number theoryprimesA2892805 sources

declared openerdos:460

Erdős problem 460

number theoryN/A2 sources

declared proved (Lean) · formalizederdos:464

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))

number theoryN/A4 sources

declared proved (Lean) · formalizederdos:476

True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (A : Finset (ZMod p)), A.restrictedSumset.card ≥ min (2 * A.card - 3) p

number theoryadditive combinatoricsN/A5 sources

declared open · formalizederdos:477

Does there exist an integer polynomial

f

of degree at least two and a set

A \subseteq \mathbb{Z}

such that every integer has a unique representation

n = a + f(k)

? A manuscript claims the thirteenth powers admit a tiling complement.

number theoryN/A4 sources

declared proved · formalizederdos:480

True ↔ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ n, Filter.liminf (fun m => ↑↑n * |x (m + ↑n) - x m|) Filter.atTop ≤ 1 / √5

number theoryN/A3 sources

declared proved (Lean) · formalizederdos:481

∀ {r : ℕ} (a b : Fin r → ℕ), (∀ (i : Fin r), 0 < a i) → 1 < ∑ i, 1 / ↑(a i) → ∃ k, ¬((Erdos481.T a b)^[k] [1]).Nodup

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:484

∃ c, 0 < c ∧ ∀ (k : ℕ), 0 < k → ∃ N₀, ∀ (N : ℕ), N₀ ≤ N → ∀ (f : ℕ → Fin k), c * ↑N ≤ ↑{n ∈ Finset.Icc 1 N | ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n}.card

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:487

True ↔ ∀ (A : Set ℕ), A.HasPosDensity → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a.lcm b = c

number theoryN/A5 sources

declared falsifiable · formalizederdos:488

True ↔ ∀ (A : Finset ℕ), A.Nonempty → 0 ∉ A → 1 ∉ A → ∀ (n m : ℕ), m > n → A.max ≤ ↑n → ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m < 2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n

number theoryN/A3 sources

declared proved (Lean)erdos:490

Erdős problem 490

number theoryA3972054 sources

declared proved (Lean) · formalizederdos:493

True ↔ ∃ k N, ∀ (n : ℤ), N ≤ n → ∃ a, (∀ (i : Fin k), 2 ≤ a i) ∧ ∏ i, a i - ∑ i, a i = n

number theoryN/A5 sources

declared solved (Lean) · formalizederdos:497

∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 2)))

combinatoricsA0003725 sources

declared proved (Lean) · formalizederdos:498

True ↔ ∀ (n : ℕ) (z : Fin n → ℂ), (∀ (i : Fin n), 1 ≤ ‖z i‖) → ∀ (c : ℂ), {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z i ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)

combinatoricsanalysisN/A5 sources

declared proved (Lean) · formalizederdos:499

True ↔ ∀ (n : ℕ), ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ, ↑n ^ (-↑n) ≤ ∏ i, M i (σ i)

combinatoricsN/A5 sources

declared open · formalizederdos:501

For every

x \in \mathbb{R}

let

A_x \subset \mathbb{R}

be a bounded set of Lebesgue outer measure

< 1

. Must there be an infinite independent set, that is an infinite

X \subseteq \mathbb{R}

with

x \notin A_y

for all distinct

x, y \in X

? Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal. The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

combinatoricsset theoryN/A4 sources

declared solved (Lean) · formalizederdos:502

∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))), A.Finite → {d | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2 → A.ncard ≤ (n + 2).choose 2

geometrydistancesA0276275 sources

declared open · formalizederdos:503

∀ (n : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} sorry

geometrydistancesA1757693 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science