lean_workbook_plus_79526

Proved

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

Solve the following system of equations over the real numbers: $2x_1 = x_5 ^2 - 23$ $4x_2 = x_1 ^2 + 7$ $6x_3 = x_2 ^2 + 14$ $8x_4 = x_3 ^2 + 23$ $10x_5 = x_4 ^2 + 34$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79526 : ∃ x : ℕ → ℝ, 2*x 1 = x 5 ^ 2 - 23 ∧ 4*x 2 = x 1 ^ 2 + 7 ∧ 6*x 3 = x 2 ^ 2 + 14 ∧ 8*x 4 = x 3 ^ 2 + 23 ∧ 10*x 5 = x 4 ^ 2 + 34   :=  by sorry

Source

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

View graph