lean_workbook_plus_17436

Proved

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

If $a+4b+9c+16d=1$ , $4a+9b+16c+25d=12$ , $9a+16b+25c+36d=123$ , find $16a+25b+36c+49d$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17436 (a b c d : ℝ) (ha : a + 4 * b + 9 * c + 16 * d = 1) (hb : 4 * a + 9 * b + 16 * c + 25 * d = 12) (hc : 9 * a + 16 * b + 25 * c + 36 * d = 123) : 16 * a + 25 * b + 36 * c + 49 * d = 334   :=  by sorry

Source

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

View graph