lean_workbook_plus_73758

Proved

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

Regard this as a linear system with the solution $(1,2,3)$ : \n \n \begin{eqnarray}1+{2\over b}-{3\over c} &=& a\-{1\over a}+2+{3\over c} &=& b\{1\over a}-{2\over b}+3 &=& c\end{eqnarray} \n Adding up all the equations we get $a+b+c=6$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73758  (a b c : ℝ)
  (h₀ : 1 + 2 / b - 3 / c = a)
  (h₁ : -1 / a + 2 + 3 / c = b)
  (h₂ : 1 / a - 2 / b + 3 = c) :
  a + b + c = 6   :=  by sorry

Source

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

View graph