lean_workbook_plus_58717

Proved

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

Consider the quadratic function $f(x)=20x^2-11x+2016$ . Show that there exists an integer $\alpha$ such that $2^{10^{11^{2016}}}\mid f(\alpha)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58717 (f : ℤ → ℤ) (α : ℤ) (hf: f = (λ x:ℤ => 20 * x ^ 2 - 11 * x + 2016)) : (¬ 2 ^ 10 ^ 11 ^ 2016 ∣ f α) ∨ ∃ α : ℤ, (2 ^ 10 ^ 11 ^ 2016 ∣ f α)   :=  by sorry

Source

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

View graph