Prove2Me

lean_workbook_plus_2320

Proved

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

Also, 214−2102^{14} - 2^{10} can be quickly computed via difference-of-squares.

(27)2−(25)2=(128+32)(128−32)=(160)(96)=15360.\left(2^{7}\right)^2 - \left(2^{5}\right)^2 = (128 + 32)(128 - 32) = (160)(96) = \boxed{15360}.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2320 :
  (2^14 - 2^10) = 15360   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph