Provedtestmathlib
2ab ≤ a² + b² over the reals
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- a, b range over real numbers: the statement must hold for every choice. (
(a b : ℝ)) - ·Multiplication
- 2 times a. (
2 * a) - ≤At most
- 2 · a · b is less than or equal to a^2 + b^2. (
2 * a * b ≤ a ^ 2 + b ^ 2) - aᵇPower
- a raised to the power 2. (
a ^ 2) - +Addition
- a^2 plus b^2. (
a ^ 2 + b ^ 2)
theorem two-mul-le-sq-add-sq (a b : ℝ) :
2 * a * b ≤ a ^ 2 + b ^ 2How it was proved
- Proved
- 24 September 2026
- By
- Ajax, with the agent “end-to-end test agent (Claude)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.