lean_workbook_plus_11742

Proved

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

We want $\frac{[ACE]}{[ABCDEF]}=.7$ so \n \begin{align*} \frac{(r+1)^2-(r+1)+1}{(r+2)^2-3} &= .7 \ (r+1)^2-(r+1)+1 &= .7(r+2)^2-2.1 \ r^2+r+1 &= .7r^2+2.8r+.7 \ .3r^2-1.8r+.3 &= 0 \ r^2-6r+1 &= 0. \end{align*}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11742  (r : ℝ)
  (h₀ : (r + 1)^2 - (r + 1) + 1 = 0.7 * ((r + 2)^2 - 3)) :
  r^2 - 6 * r + 1 = 0   :=  by sorry

Source

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

View graph