Binomial coefficients are not perfect powers

Proved

ProofsInTheBook.Chapter03.chapter03_erdos

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\ge2$ ,

\binom nk\ne m^\ell.

The base m is an arbitrary natural number.

Preamble

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

Formal statement

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

Source

Formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter03.lean#L5628. This is a chapter headline concerning binomial coefficients and their prime factors. Topic reference: Martin Aigner and Günter M. Ziegler, Proofs from THE BOOK, 6th edition, Springer, 2018, Chapter 3, “Binomial coefficients are (almost) never powers”, pp. 15–18 (https://doi.org/10.1007/978-3-662-57265-8_3).

View graph