lean_workbook_plus_7594

Proved

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

Let $p(x) = x^2+ax+b$ be a quadratic polynomial with $a,b\in\mathbb{Z}$ .Given any integer $n$ ,Show that there is an integer $M$ such that $p(n) p(n+1) = p(M)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7594 (p : ℤ → ℤ) (a b n : ℤ) (hp : ∀ x : ℤ, p x = x^2 + a * x + b) : ∃ M : ℤ, p n * p (n + 1) = p M   :=  by sorry

Source

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

View graph