Binomial coefficients are not powers of exponent at least three

Proved

ProofsInTheBook.Chapter03.chapter03_erdos_ge3

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

book-chapter-3lean4number-theoryproofs-from-the-book

For all $n,k,\ell,m\in\mathbb N$ satisfying $k\ge4$ , $2k\le n$ , and $\ell\ge3$ ,

\binom nk\ne m^\ell.

Preamble

import Mathlib
import Definitions.Def_ProofsInTheBook_Chapter03
open Nat
open ProofsInTheBook.Chapter03

Formal statement

theorem ProofsInTheBook.Chapter03.chapter03_erdos_ge3
    {n k l m : ℕ} (hk : 4 ≤ k) (hn : 2 * k ≤ n) (hl : 3 ≤ l) :
    n.choose k ≠ m ^ l := by sorry

Source

Formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter03.lean#L5395. This is a selected result in the local development concerning binomial coefficients and their prime factors. The specific technical formulation is cited to the repository, without claiming that it appears verbatim in the textbook.

View graph