lean_workbook_plus_10419
ProvedSolve the system in $\mathbb{Q}$ (or prove that there exist infinitely many solutions to this): $a + b + c = a^{2} + b^{2} + c^{2} = 1$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10419 (a b c : ℚ) (ha : a + b + c = 1) (hb : a^2 + b^2 + c^2 = 1) : ∃ a b c : ℚ, a + b + c = 1 ∧ a^2 + b^2 + c^2 = 1 := by sorry
Source