Prove2Me

lean_workbook_plus_11507

Proved

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

Solve for a, b, and c in the equation k1(abc)+k2(ab+ac+bc)+k3(a+b+c)+k4=0k_1(abc) + k_2(ab + ac + bc) + k_3(a+b+c) + k_4=0, where kik_i are given constants.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11507 (k₁ k₂ k₃ k₄ a b c : ℝ) : k₁ * a * b * c + k₂ * (a * b + a * c + b * c) + k₃ * (a + b + c) + k₄ = 0 → a = a ∧ b = b ∧ c = c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph