Prove2Me

lean_workbook_plus_75324

Proved

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

P(3π4)=(22)3(−22)3(1+(22)6)(1+(−22)6)=−1898⋅98=−881P\left(\frac{3\pi}{4}\right)=\dfrac{\left(\frac{\sqrt{2}}{2}\right)^3\left(\frac{-\sqrt{2}}{2}\right)^3}{\left(1+\left(\frac{\sqrt{2}}{2}\right)^6\right)\left(1+\left(-\frac{\sqrt{2}}{2}\right)^6\right)}=\dfrac{-\frac{1}{8}}{\frac{9}{8}\cdot\frac{9}{8}}=-\dfrac{8}{81} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75324 :
  ((Real.sqrt 2 / 2)^3 * (-Real.sqrt 2 / 2)^3) / ((1 + (Real.sqrt 2 / 2)^6) * (1 + (-Real.sqrt 2 / 2)^6)) = -8 / 81   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph