The twenty-ninth Mersenne number is composite
ProvedWorkbookSource.plus_78615lean-workbooksource-checked
Prove that is not a prime number.
Source: InternLM Lean-Workbook, record lean_workbook_plus_78615 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_78615 : ¬ Nat.Prime (2^29 - 1) := by sorry
Source