Prove2Me

lean_workbook_plus_1536

Proved

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

Solve the system of equation for x1,x2,x3,x4∈Rx_1,x_2,x_3,x_4\in \mathbb{R}\n

{x1+x2x3x4=2 x2+x3x4x1=2 x3+x4x1x2=2 x4+x1x2x3=2\begin{cases}x_1+x_2x_3x_4=2 \ x_2+x_3x_4x_1=2 \ x_3+x_4x_1x_2=2 \ x_4+x_1x_2x_3=2\end{cases}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1536 (x : ℕ → ℝ) : (∃ x_1 x_2 x_3 x_4 :ℝ, x_1 + x_2 * x_3 * x_4 = 2 ∧ x_2 + x_3 * x_4 * x_1 = 2 ∧ x_3 + x_4 * x_1 * x_2 = 2 ∧ x_4 + x_1 * x_2 * x_3 = 2) ↔ (∃ x_1 x_2 x_3 x_4 :ℝ, x_1 + x_2 * x_3 * x_4 = 2 ∧ x_2 + x_3 * x_4 * x_1 = 2 ∧ x_3 + x_4 * x_1 * x_2 = 2 ∧ x_4 + x_1 * x_2 * x_3 = 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph