lean_workbook_plus_46033

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Induction: \n\n $n = 5 \implies 32 > 25$ which is obviously true. \n\n Assume it holds for $n = k$ \n\n $2^k > k^2$ \n\n Now since $k > 4, (k-1)^2 > 2 \implies k^2 > 2k+1 \implies 2k^2 > (k+1)^2$ \n\n From our inductive hypothesis, $2^k > k^2 \implies 2^{k+1} > 2k^2 > (k+1)^2$ from our result above. \n\n Therefore, $2^n > n^2$ for all $n > 4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46033  (n : ℕ)
  (h₀ : 5 ≤ n) :
  (2^n) > n^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph