Compfiles: Catalog Of Math Problems Formalized In Lean

Singapore2019P11


import Mathlib

/-!
# Singapore Math Olympiad (Senior) 2019 (Round 1), Problem 11

http://www.realsutra.com/limjeck/SMO_Senior_2019.pdf

Find the value of 448 * (sin 12 degrees) * (sin 39 degrees) * (sin 51 degrees) / sin 24 degrees
-/
open Real

namespace Singapore2019R1P11

noncomputable /- determine -/ abbrev solution : ℝ := sorry

theorem singapore2019_r1_p11 : 448 * sin (12 * π / 180) * sin (39 * π / 180) * sin (51 * π / 180) / sin (24 * π / 180) = solution := sorry

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: