Vela Mathematics Program: problems

Problem ledger

1,217 problems · 9/25Number SourcesGraph view

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 · formalizederdos:402

∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card

number theoryN/A2 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:404

Erdős problem 404

number theoryfactorialsN/A

declared provederdos:405

Erdős problem 405

number theoryfactorialsN/A

declared open · formalizederdos:406

True ↔ {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1]}.Finite

number theorybase representationsN/A2 sources

declared provederdos:407

Erdős problem 407

number theorypossible · A387688

declared openerdos:408

Erdős problem 408

number theoryiterated functionsA049108

declared open · formalizederdos:409

∀ (n : ℕ), 0 < n → IsLeast {i | Nat.Prime ((fun x => x.totient + 1)^[i] n)} sorry

number theoryiterated functionsA039651 · A2294872 sources

declared open · formalizederdos:410

True ↔ ∀ n > 1, Filter.Tendsto (fun k => ↑((⇑(ArithmeticFunction.sigma 1))^[k] n) ^ (1 / ↑k)) Filter.atTop Filter.atTop

number theoryiterated functionsA007497 · possible2 sources

declared openerdos:411

Erdős problem 411

number theoryiterated functionsA383044 · possible2 sources

declared open · formalizederdos:412

True ↔ ∀ m ≥ 2, ∀ n ≥ 2, ∃ i j, (⇑(ArithmeticFunction.sigma 1))^[i] m = (⇑(ArithmeticFunction.sigma 1))^[j] n

number theoryiterated functionsA007497 · A0515722 sources

declared open · formalizederdos:413

True ↔ {n | Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardDistinctFactors m)) n}.Infinite

number theoryiterated functionsA0052362 sources

declared open · formalizederdos:414

True ↔ ∀ m > 0, ∀ n > 0, ∃ i j, Erdos414.h^[i] m = Erdos414.h^[j] n

number theoryiterated functionsA064491 · possible2 sources

declared openerdos:415

Erdős problem 415

number theorypossible2 sources

declared open · formalizederdos:416

Filter.Tendsto (fun x => Erdos416.V (2 * x) / Erdos416.V x) Filter.atTop (nhds 2)

number theoryA2648102 sources

declared open · formalizederdos:417

True ↔ ∃ L, Filter.Tendsto (fun x => ↑{k | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard / ↑(Nat.totient '' {m | 1 ≤ m ∧ ↑m ≤ x}).ncard) Filter.atTop (nhds L)

number theoryA264810 · A0610702 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:420

Erdős problem 420

number theoryN/A

declared open · formalizederdos:421

True ↔ ∃ d, StrictMono d ∧ 1 ≤ d 0 ∧ (Set.range d).HasDensity 1 ∧ Set.InjOn (fun x => match x with | (u, v) => ∏ i ∈ Finset.Icc u v, d i) {(u, v) | u ≤ v}

number theoryA389544 · A3908482 sources

declared open · formalizederdos:422

True ↔ {n | ∀ (x : ℕ+), Erdos422.f x ≠ n}.Infinite

number theoryA0051852 sources

declared openerdos:423

Erdős problem 423

number theoryA0052432 sources

declared open · formalizederdos:424

Let

a_1 = 2

and

a_2 = 3

and continue the sequence by appending to

a_1, \dots, a_n

all possible values of

a_ia_j - 1

with

i \ne j

. Is it true that the set of integers which eventually appear has positive density?

number theoryA0052444 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 open · formalizederdos:428

True ↔ ∃ A, (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧ Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0

number theoryprimesN/A2 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:430

Erdős problem 430

number theorypossible

declared openerdos:431

Erdős problem 431

number theoryprimesN/A

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

Erdős problem 436

number theoryA000445 · possible

declared provederdos:437

Erdős problem 437

number theorypossible

declared solvederdos:438

Erdős problem 438

number theoryA363069

declared provederdos:439

Erdős problem 439

number theoryramsey theoryN/A

declared solvederdos:440

Erdős problem 440

number theoryN/A

declared disprovederdos:441

Erdős problem 441

number theoryA0685092 sources

declared disproved · formalizederdos:442

False ↔ ∀ (A : Set ℕ), Filter.Tendsto (fun x => 1 / Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x) * ∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun x => 1 / (∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2 * ∑ nm ∈ (Erdos442.Set.bddProdUpper A x).toFinset, 1 / ↑(nm.1.lcm nm.2)) Filter.atTop Filter.atTop

number theoryN/A2 sources

declared proved (Lean) · formalizederdos:443

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

number theoryN/A5 sources

declared provederdos:444

Erdős problem 444

number theorydivisorsN/A

declared open · formalizederdos:445

True ↔ ∀ c > 1 / 2, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445.Erdos445Prop c p n

number theoryN/A2 sources

declared solvederdos:446

Erdős problem 446

number theorydivisorsA074738

declared proved (Lean) · formalizederdos:447

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

combinatoricspossible5 sources

declared disproved · formalizederdos:448

False ↔ ∀ (ε : ℝ), 0 < ε → {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1

number theorydivisorsA3974332 sources

declared disprovederdos:449

Erdős problem 449

number theorydivisorspossible

declared open · formalizederdos:450

How large must

y(\varepsilon, n)

be so that every interval

(x, x+y)

contains at most

\varepsilon y

integers having a divisor in

(n, 2n)

? The candidate proof gives the sharp fixed-

\varepsilon

order

y = \Theta_\varepsilon(n)

, uniformly in the translate.

number theorydivisorsN/A4 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science