lean_workbook_plus_1392

Proved

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

Find all solutions $x_1, x_2, x_3, x_4, x_5$ of the system $x_5+x_2=yx_1$ $x_1+x_3=yx_2$ $x_2+x_4=yx_3$ $x_3+x_5=yx_4$ $x_4+x_1=yx_5$ where $y$ is a parameter.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1392 (y : ℝ) (x : ℕ → ℝ) : (∃ x₁ x₂ x₃ x₄ x₅ : ℝ, x₅ + x₂ = y * x₁ ∧ x₁ + x₃ = y * x₂ ∧ x₂ + x₄ = y * x₃ ∧ x₃ + x₅ = y * x₄ ∧ x₄ + x₁ = y * x₅) ↔ (∃ x : ℝ, 2 * x = y)   :=  by sorry

Source

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

View graph