Prove2Me

Cosine exceeds sine before pi over four

Proved
WorkbookRestored.plus_40

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every real angle 0<θ<π/40<\theta<\pi/4,

cos⁡θ>sin⁡θ.\cos\theta>\sin\theta.

Formalization Note This restores source entry lean_workbook_plus_40 from the Apache-2.0 Lean-Workbook dataset. The mathematical proposition is unchanged; targeted imports and namespace openings supply the constants missing from the original Prove2Me node ddeae32b-26bb-4b03-9b22-6afd34b69fdd. This is a separate corrected node because formal statements and preambles are immutable.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Tactic
open Real
Formal statement
theorem WorkbookRestored.plus_40 :
  ∀ θ : ℝ, 0 < θ ∧ θ < Real.pi / 4 → Real.cos θ > Real.sin θ   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_40; original Prove2Me theorem ID ddeae32b-26bb-4b03-9b22-6afd34b69fdd; Apache-2.0.

View graph