Back to Problems
johnson_chromaticNumber_odd
Specification
It can be seen that the chromatic number of $J(2k,k)$ is $>k+1$ for all odd $k>2$.
Lean 4 Statement
theorem johnson_chromaticNumber_odd (k : ℕ) (hk : 2 < k) (h : Odd k) :
k + 1 < J(2 * k, k).chromaticNumber
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.