lean_workbook_plus_27037

Proved

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

Solve the system of equations: \n $8 = A + B + C + D$ \n $16 = A + 2B + 4C + 8D$ \n $0 = A + 3B + 9C + 27D$ \n $-64 = A + 4B + 16C + 64D$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27037 (A B C D : ℝ) : (8 = A + B + C + D ∧ 16 = A + 2*B + 4*C + 8*D ∧ 0 = A + 3*B + 9*C + 27*D ∧ -64 = A + 4*B + 16*C + 64*D) ↔ A = 0 ∧ B = 0 ∧ C = 12 ∧ D = -4   :=  by sorry

Source

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

View graph