Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×combinatorics ×Clear all

Problem ledger

19 problemsGraph view
declared open · formalized · $1000erdos:20
sorry ↔ ∃ c, ∀ (n k : ℕ), n > 0 → Erdos20.f n k < c k ^ n
combinatoricsA3320772 sources
declared open · formalized · $100erdos:120
True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A
combinatoricsN/A3 sources
declared open · $500erdos:161
Erdős problem 161
combinatoricsramsey theorydiscrepancyN/A2 sources
declared openerdos:162
Erdős problem 162
combinatoricsramsey theorydiscrepancyN/A
declared open · formalizederdos:501
For every x∈Rx \in \mathbb{R} let Ax⊂RA_x \subset \mathbb{R} be a bounded set of Lebesgue outer measure <1< 1. Must there be an infinite independent set, that is an infinite X⊆RX \subseteq \mathbb{R} with x∉Ayx \notin A_y for all distinct x,y∈Xx, 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:602
¬Erdos602.disjoint_without_infinite_claim
combinatoricsset theoryN/A3 sources
declared open · formalizederdos:624
Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop
combinatoricspossible2 sources
declared openerdos:644
Erdős problem 644
combinatoricspossible
declared openerdos:665
Erdős problem 665
combinatoricsN/A2 sources
declared open · formalizederdos:701
True ↔ ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)), IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}
combinatoricsintersecting familyN/A2 sources
declared openerdos:724
Erdős problem 724
combinatoricsA001438
declared openerdos:725
Erdős problem 725
combinatoricsA001009
declared openerdos:734
Erdős problem 734
combinatoricspossible2 sources
declared openerdos:776
Erdős problem 776
combinatoricspossible2 sources
declared open · formalizederdos:857
have f := sorry; ∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun n => ↑(Erdos857.m n k) / f k n) Filter.atTop (nhds 1)
combinatoricspossible2 sources
declared openerdos:901
Erdős problem 901
combinatoricshypergraphspossible
declared openerdos:1159
Erdős problem 1159
combinatoricsN/A
declared openerdos:1173
Erdős problem 1173
set theorycombinatoricsN/A
declared openerdos:1183
Erdős problem 1183
combinatoricsramsey theorypossible2 sources

Search problems.science

Find a Problem, Result, source, or page