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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

15 declarations, 10 contain sorry, 0 declared as axioms

Erdős Problem 835

References:

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Erdos835.Property The property that for a given $k$, the $k$-subsets of a $2k$-set can be colored with $k+1$ colors such that any $(k+1)$-subset contains all colors line 40 source
Source documentation
The property that for a given $k$, the $k$-subsets of a $2k$-set can be colored with $k+1$ colors such that any $(k+1)$-subset contains all colors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Finset, Fin, HMul.hMul, OfNat.ofNat, Eq, Finset.card, Exists, HAdd.hAdd, Finset.image, Finset.filter, LT.lt, Finset.univ
15 instances, coercions and auxiliary constants left out.
```
def Property (k : ℕ) : Prop :=
…
```
theorem Erdos835.erdos_835 Documented declaration: erdos_835 sorry line 52 source
Source documentation
Does there exist a $k>2$ such that the $k$-sized subsets of {1,...,2k} can be coloured with $k+1$ colours such that for every $A\subset \{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$-sized subsets of $A$?

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, GT.gt, OfNat.ofNat, Erdos835.Property
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_835 : answer(sorry) ↔ ∃ k > 2, Property k := by
…
```
Mentions: Erdos835.Property
theorem Erdos835.property_iff_chromaticNumber sorry line 56 source
depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Eq, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Finset.card, SimpleGraph.johnson, HAdd.hAdd, Erdos835.Property
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos835.erdos_835.variants.johnson Alternative statement of Erdős Problem 835 using the chromatic number of the Johnson graph sorry line 67 source
Source documentation
Alternative statement of Erdős Problem 835 using the chromatic number of the Johnson graph. This is equivalent to asking whether there exists $k > 2$ such that the chromatic number of the Johnson graph $J(2k, k)$ is $k+1$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Eq, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Finset.card, SimpleGraph.johnson
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_835.variants.johnson : answer(sorry) ↔ ∃ l,
    -- making sure k > 2
    letI k := l + 3
…
```
theorem Erdos835.johnsonGraph_2k_k_chromaticNumber_known_cases It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs sorry line 78 source
Source documentation
It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

L4DEL explanation
It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, GT.gt, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem johnsonGraph_2k_k_chromaticNumber_known_cases (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 8) :
    J(2 * k, k).chromaticNumber > k + 1 := by
…
```
theorem Erdos835.johnsonGraph_18_9_chromaticNumber The smallest case not on this page is $k=9$: But that one can be solved as well: The chromatic number of $J(18, 9)$ is at least $11$ sorry line 88 source
Source documentation
The smallest case not on this page is $k=9$: But that one can be solved as well: The chromatic number of $J(18, 9)$ is at least $11$.

depends on sorry what this means
Statement uses: GT.gt, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, OfNat.ofNat, Nat, Eq, Finset.card, SimpleGraph.johnson, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem johnsonGraph_18_9_chromaticNumber : J(18, 9).chromaticNumber > 9 + 1 := by
…
```
def Erdos835.johnsonBound Johnson's upper bound on the maximum size A(n, d, w) of a n-dimensional binary code of distance d and weight w is as follows: * If d > 2 * w, then A(n, d, w) = 1 line 95 source
Source documentation
Johnson's upper bound on the maximum size A(n, d, w) of a n-dimensional binary code of distance d and weight w is as follows:
- If d > 2 * w, then A(n, d, w) = 1.
- If d ≤ 2 * w, then A(n, d, w) ≤ ⌊n / w * A(n - 1, d, w - 1)⌋.
no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def johnsonBound : ℕ → ℕ → ℕ → ℕ
  | 0, _d, _w => 1
  | _n, _d, 0 => 1
  | n + 1, d, w + 1 => if 2 * (w + 1) < d then 1 else (n + 1) * johnsonBound n d w / (w + 1)

/-- Johnson's bound for the independence number of the Johnson graph. -/
@[category research solved, AMS 5]
```
Mentions: AMS
lemma Erdos835.indepNum_johnson_le_johnsonBound Johnson's bound for the independence number of the Johnson graph sorry line 102 source
Source documentation
Johnson's bound for the independence number of the Johnson graph.

depends on sorry what this means
Statement uses: Nat, LE.le, SimpleGraph.indepNum, Subtype, Finset, Fin, Eq, Finset.card, SimpleGraph.johnson, Erdos835.johnsonBound, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
```
lemma indepNum_johnson_le_johnsonBound : α(J(n, k)) ≤ johnsonBound n 4 k := sorry
…
```
Mentions: Erdos835.johnsonBound
lemma Erdos835.div_johnsonBound_le_chromaticNum_johnson Johnson's bound for the chromatic number of the Johnson graph line 106 source
Source documentation
Johnson's bound for the chromatic number of the Johnson graph.

depends on sorry what this means
Statement uses: Nat, LE.le, ENat, Nat.ceil, NNRat, HDiv.hDiv, Nat.choose, Erdos835.johnsonBound, OfNat.ofNat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, Eq, Finset.card, SimpleGraph.johnson
Proof uses: LT.lt, Or, lt_or_ge, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.choose_eq_zero_of_lt, CharP.cast_eq_zero, zero_div, Nat.ceil_zero, Nonempty, Eq.mpr, Exists, id, Eq.mp, Finset.Nonempty, Finset.powersetCard, Finset.univ and 20 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma div_johnsonBound_le_chromaticNum_johnson :
    ⌈(n.choose k / johnsonBound n 4 k : ℚ≥0)⌉₊ ≤ χ(J(n, k)) := by
…
```
Mentions: Erdos835.johnsonBound
theorem Erdos835.chromaticNumber_johnson_2k_k_lower_bound It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs sorry line 117 source
Source documentation
It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

L4DEL explanation
It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, ENat, HAdd.hAdd, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem chromaticNumber_johnson_2k_k_lower_bound (hk : 3 ≤ k) (hk' : k ≤ 8) :
    k + 1 < J(2 * k, k).chromaticNumber := by
…
```
theorem Erdos835.chromaticNumber_johnson_2k_k_lower_bound_odd It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs line 124 source
Source documentation
It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

L4DEL explanation
It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Odd, LT.lt, ENat, HAdd.hAdd, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson
Proof uses: lt_imp_lt_of_le_of_le, Nat.ceil, NNRat, HDiv.hDiv, Nat.choose, Erdos835.johnsonBound, le_refl, Erdos835.div_johnsonBound_le_chromaticNum_johnson
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem chromaticNumber_johnson_2k_k_lower_bound_odd (hk : 3 ≤ k) (hk' : k ≤ 300) (hk_odd : Odd k) :
    k + 1 < J(2 * k, k).chromaticNumber := by
…
```
theorem Erdos835.johnson_chromaticNumber_odd It can be seen that the chromatic number of $J(2k,k)$ is $>k+1$ for all odd $k>2$ sorry line 133 source
Source documentation
It can be seen that the chromatic number of $J(2k,k)$ is $>k+1$ for all odd $k>2$.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Odd, ENat, HAdd.hAdd, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.
```
theorem johnson_chromaticNumber_odd (k : ℕ) (hk : 2 < k) (h : Odd k) :
    k + 1 < J(2 * k, k).chromaticNumber :=
…
```
theorem Erdos835.johnson_chromaticNumber_composite Ma and Tang have proved that the chromatic number of $J(2k,k)$ is $>k+1$ for all $k>2$ not of the form $p-1$ for prime $p$ sorry line 142 source
Source documentation
Ma and Tang have proved that the chromatic number of $J(2k,k)$ is $>k+1$ for all $k>2$ not of the form $p-1$ for prime $p$.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Composite, HAdd.hAdd, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.
```
theorem johnson_chromaticNumber_composite (k : ℕ) (hk : 2 < k) (h : (k + 1).Composite) :
    k + 1 < J(2 * k, k).chromaticNumber :=
…
```
theorem Erdos835.johnsonGraph_chromaticNumber_odd_of_johnson_chromaticNumber_composite Ma and Tang's result implies the cases for odd $k$ line 150 source
Source documentation
Ma and Tang's result implies the cases for odd $k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Composite, HAdd.hAdd, ENat, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson, Odd
Proof uses: And.intro, Not, Nat.Prime, Decidable.byContradiction, Eq.mpr, Exists, And, Dvd.dvd, LE.le, id, congrArg, propext, Nat.not_prime_iff_exists_dvd_lt, Exists.intro, Iff.mp, Even, even_iff_two_dvd, Odd.add_one
49 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem johnsonGraph_chromaticNumber_odd_of_johnson_chromaticNumber_composite :
    (type_of% johnson_chromaticNumber_composite) → (type_of% johnson_chromaticNumber_odd) := by
…
```
Mentions: Erdos835.johnson_chromaticNumber_composite, Erdos835.johnson_chromaticNumber_odd
theorem Erdos835.johnson_chromaticNumber Is the chromatic number of J(2 * k, k) always at least k + 2? sorry line 162 source
Source documentation
Is the chromatic number of J(2 * k, k) always at least k + 2?

depends on sorry what this means
Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, LE.le, ENat, HAdd.hAdd, SimpleGraph.chromaticNumber, Subtype, Finset, Fin, HMul.hMul, Eq, Finset.card, SimpleGraph.johnson
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.
```
theorem johnson_chromaticNumber : answer(sorry) ↔
    ∀ k ≥ 3, k + 2 ≤ J(2 * k, k).chromaticNumber :=
…
```