FormalConjectures/ErdosProblems/664.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
3 declarations, 3 contain sorry, 0 declared as axioms
Erdős Problem 664
References:
- erdosproblems.com/664
- [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
- [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.
Imports (1)
- theorem
Erdos664.erdos_664sorry line 52 sourcedepends on sorry what this means
Statement uses:
Iff,False,Real,LT.lt,OfNat.ofNat,Exists,Nat,Fin,Finset,HMul.hMul,Real.sqrt,Finset.card,Ne,LE.le,Inter.inter,And,Finset.NonemptyProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous26 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
- theorem
Erdos664.erdos_664.variants.two_fifthssorry line 62 sourcedepends on sorry what this means
Statement uses:
Not,Exists,Nat,Fin,Finset,LT.lt,Real,HMul.hMul,HDiv.hDiv,OfNat.ofNat,Real.sqrt,Finset.card,Ne,LE.le,Inter.inter,And,Finset.NonemptyProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous30 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
- theorem
Erdos664.erdos_664.variants.block_designIn [Er81] the condition sorry line 77 sourceSource documentation
In [Er81] the condition $\lvert A_i\cap A_j\rvert\leq 1$ for all $i\neq j$ is replaced by every two points in $\{1,\ldots,n\}$ being contained in exactly one $A_i$, that is, $A_1,\ldots,A_m$ is a pairwise balanced block design. The bound $\lvert A_i\rvert>c\sqrt{n}$ is kept, only the condition $c<1$ is omitted. This weaker version remains open, although Alon conjectures the answer there to also be no.
depends on sorry what this means
Statement uses:
Iff,True,Real,LT.lt,OfNat.ofNat,Exists,Nat,Fin,Finset,HMul.hMul,Real.sqrt,Finset.card,Ne,ExistsUnique,And,Membership.mem,Finset.Nonempty,Inter.inter,LE.leProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous25 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_664.variants.block_design : answer(sorry) ↔ ∀ c : ℝ, 0 < c → ∃ K : ℕ, ∀ (n m : ℕ) (A : Fin m → Finset (Fin n)), (∀ i, c * √n < (A i).card) → (∀ x y : Fin n, x ≠ y → ∃! i, x ∈ A i ∧ y ∈ A i) → ∃ B : Finset (Fin n), (∀ i, (B ∩ A i).Nonempty) ∧ ∀ i, (B ∩ A i).card ≤ K := by …Mentions: c