lean_workbook_plus_10782

Proved

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

The equation is equivalent to: \n\n

n^4=n^3+13n^2+36n+39

And in part a we have proved that $n$ must be a multiple of 3 to be a solution. So the LHS is divisible by 9 and each of the terms $n^3 , 13n^2 , 36n$ is divisible by 9. But 39 is not divisible by 9 so the RHS is not a multiple of 9. Contradiction. There is no solution in positive integers

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10782  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : 3∣n)
  (h₂ : n^4 = n^3 + 13 * n^2 + 36 * n + 39) :
  False   :=  by sorry

Source

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

View graph