Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 5/13Number SourcesGraph view

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

Erdős problem 436

number theoryA000445 · possible

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

Erdős problem 467

number theoryN/A

declared openerdos:468

Erdős problem 468

number theorydivisorsA167485 · A387502 · A387503

declared open · formalized · $10erdos:470

sorry ↔ ∃ n, n.Weird ∧ Odd n

number theorydivisorsA006037 · A0029752 sources

declared openerdos:472

Erdős problem 472

number theoryA389713 · possible

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

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

declared open · formalizederdos:486

True ↔ ∀ (X : (n : ℕ) → Set (ZMod n)), ∃ d, {m | ∀ (n : ℕ), ↑m ∉ X n}.HasLogDensity d

number theoryprimitive setsN/A2 sources

declared open · formalizederdos:489

A

is a forbidden-divisor set with

|A \cap [1,x]| = o(\sqrt{x})

and

B = \{b_1 < b_2 < \cdots\}

the sifted set, must

x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2

converge to a finite limit?

number theoryN/A4 sources

declared open · formalizederdos:495

True ↔ ∀ (α β : ℝ), Filter.liminf (fun n => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0

diophantine approximationnumber theoryN/A2 sources

declared open · $500erdos:500

Erdős problem 500

graph theoryhypergraphsturan numberA140462

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 open · formalizederdos:503

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

geometrydistancesA1757693 sources

declared open · formalizederdos:507

Asymptotics.IsEquivalent Filter.atTop Erdos507.α sorry

geometryN/A3 sources

declared open · formalizederdos:508

4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber

geometryramsey theoryN/A2 sources

declared open · formalizederdos:509

∀ {M : Type u} [inst : MetricSpace M] (S : Set M), S.Nonempty → ∀ (r : ℝ) (ι : Type v) (bdc : Erdos509.BoundedDiscCover S r ι), 0 < r

analysisN/A2 sources

declared open · formalizederdos:510

sorry ↔ ∃ c, ∃ (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ θ, ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N

analysisN/A2 sources

declared open · formalizederdos:513

sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

analysisN/A3 sources

declared openerdos:514

For a transcendental entire function, how fast can

|f(z)|

be forced to grow along a path to infinity, and how short can such a path be in terms of the maximum modulus

M(r, f)

analysisN/A4 sources

declared open · formalizederdos:517

sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (k : ℕ), a k ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x | f x = z}.Infinite

analysisN/A3 sources

declared open · formalizederdos:520

True ↔ ∃ c > 0, ∀ (Ω : Type) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (f : ℕ → Ω → ℝ), Erdos520.IsRademacherMultiplicative f → ∀ᵐ (ω : Ω), Filter.limsup (fun N => ∑ m ∈ Finset.Iic N, f m ω / √(↑N * Real.log (Real.log ↑N))) Filter.atTop = c

number theoryprobabilityN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science