Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1961P2

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1961, Problem 2

Let $a, b, c$ be the sides of a triangle, and $T$ its area. Prove:
$$ a^2 + b^2 + c^2 \ge 4\sqrt{3} T $$
Equality holds if and only if the triangle is equilateral.
-/

namespace Imo1961P2

/--
**IMO 1961 P2 (Inequality Case)**
-/
theorem imo1961_p2a (a b c T : ℝ)
    (h_pos_a : 0 < a) (h_pos_b : 0 < b) (h_pos_c : 0 < c)
    (h_area : 16 * T^2 = (a + b + c) * (a + b - c) * (a - b + c) * (-a + b + c)) :
    a^2 + b^2 + c^2 ≥ 4 * Real.sqrt 3 * T := sorry

/--
**IMO 1961 P2 (Equality Case)**
-/
theorem imo1961_p2b (a b c T : ℝ)
    (h_pos_a : 0 < a) (h_pos_b : 0 < b) (h_pos_c : 0 < c) (h_pos_T : 0 < T)
    (h_area : 16 * T^2 = (a + b + c) * (a + b - c) * (a - b + c) * (-a + b + c)) :
    a^2 + b^2 + c^2 = 4 * Real.sqrt 3 * T ↔ a = b ∧ b = c := sorry

end Imo1961P2

File author(s): lean-tom (with assistance from Gemini)

This problem has a complete formalized solution.