A hypothetical perfect power forces n above k to that exponent

Proved

ProofsInTheBook.Chapter03.erdos_step1_n_gt_k_pow

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

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

Let $n,k,\ell,m\in\mathbb N$ satisfy $k\ge4$ , $2k\le n$ , $\ell\ge2$ , and $\binom nk=m^\ell$ . Then

k^\ell<n.

Preamble

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

Formal statement

lemma ProofsInTheBook.Chapter03.erdos_step1_n_gt_k_pow {n k l m : ℕ} (hk : 4 ≤ k) (hn : 2 * k ≤ n)
    (hl : 2 ≤ l) (h_eq : n.choose k = m ^ l) : k ^ l < n := by sorry

Source

Formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter03.lean#L4124. 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