Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 6/12Number SourcesGraph view

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

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

Erdős problem 452

number theorypossible

declared disproved (Lean) · formalizederdos:453

False ↔ Erdos453.EventuallyHasPrimeWitness

number theoryN/A5 sources

declared open · formalizederdos:454

True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

number theoryprimesA389676 · A3896772 sources

declared open · formalizederdos:455

True ↔ ∀ (q : ℕ → ℕ), StrictMono q → (∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) → Filter.Tendsto (fun n => ↑(q n) / ↑n ^ 2) Filter.atTop Filter.atTop

number theoryN/A2 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 falsifiable · formalizederdos:458

True ↔ ∀ (k : ℕ), Erdos458.lcm_upto (Nat.nth Prime (k + 1) - 1) < Nat.nth Prime k * Erdos458.lcm_upto (Nat.nth Prime k)

number theoryprimesA0566042 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 openerdos:461

Erdős problem 461

number theoryprimespossible

declared openerdos:462

Erdős problem 462

number theoryprimesA032742 · possible

declared open · formalizederdos:463

True ↔ ∃ f, ∃ (_ : Filter.Tendsto f Filter.atTop Filter.atTop), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, m.Composite ∧ n + f n < m ∧ m < n + m.minFac

number theoryprimespossible2 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 provederdos:465

Erdős problem 465

number theoryN/A

declared provederdos:466

Erdős problem 466

number theoryN/A

declared openerdos:467

Erdős problem 467

number theoryN/A

declared openerdos:468

Erdős problem 468

number theorydivisorsA167485 · A387502 · A387503

declared proved (Lean) · formalizederdos:469

Does the sum of the reciprocals of all primitive pseudoperfect numbers converge?

number theorydivisorsA006036 · A119425 · possible5 sources

declared open · formalized · $10erdos:470

sorry ↔ ∃ n, n.Weird ∧ Odd n

number theorydivisorsA006037 · A0029752 sources

declared provederdos:471

Erdős problem 471

number theorypossible

declared openerdos:472

Erdős problem 472

number theoryA389713 · possible

declared provederdos:473

Erdős problem 473

number theoryA055265

declared decidableerdos:475

Erdős problem 475

number theoryadditive combinatoricsN/A

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

Erdős problem 478

number theoryfactorialsA210184

declared open · formalizederdos:479

sorry ↔ ∀ k > 1, {n | 2 ^ n ≡ k [MOD n]}.Infinite

number theoryA036236 · A015919 · A050259 · A015921 · A006521 · A006517 · A0159402 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 solvederdos:482

Erdős problem 482

number theoryA004539

declared openerdos:483

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

Problems · Vela Mathematics Program

Problem ledger

Search problems.science