Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×combinatorics ×Clear all

Problem ledger

4 problemsGraph view
declared proved (Lean) · formalizederdos:447
True ↔ (fun n => ↑(Erdos447.maxUnionFree n)) =o[Filter.atTop] fun n => 2 ^ n
combinatoricspossible5 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 proved (Lean) · formalizederdos:1022
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
combinatoricshypergraphspossible6 sources

Search problems.science

Find a Problem, Result, source, or page