lean_workbook_plus_63103

Disproved

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

Let $f(x)=ax^4+bx^3+cx^2+dx+e$ with $f(x)=\frac{1}{x^2(x+1)}$ for $x=1,2,3,4,5$ \n\n Let $g(x)=x^2(x+1)f(x)-1$ obviously $g(x)$ has factor $(x-1)(x-2)(x-3)(x-4)(x-5)$ so we can write $g(x)=A(x-1)(x-2)(x-3)(x-4)(x-5)$ \n\n $x^2(x+1)f(x)-1=A(x-1)(x-2)(x-3)(x-4)(x-5)$ take $x=-1$ \n\n $-1=A(-6!)\implies A=\frac{1}{720}$ \n\n $f(x)=\frac{(x-1)(x-2)(x-3)(x-4)(x-5)+720}{720x^2(x+1)}=\frac{x^4-16x^3+101x^2-326x+600}{720x^2}$ \n\n $20(a-b+c-d+e) =20f(-1)=20\cdot \frac{1044}{720}=29$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63103  (a b c d e : ℝ)
  (f : ℝ → ℝ)
  (h₀ : ∀ x, f x = a * x^4 + b * x^3 + c * x^2 + d * x + e)
  (h₁ : f 1 = 1 / (1^2 * (1 + 1)))
  (h₂ : f 2 = 1 / (2^2 * (2 + 1)))
  (h₃ : f 3 = 1 / (3^2 * (3 + 1)))
  (h₄ : f 4 = 1 / (4^2 * (4 + 1)))
  (h₅ : f 5 = 1 / (5^2 * (5 + 1))) :
  20 * (a - b + c - d + e) = 29   :=  by sorry

Source

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

View graph