LeanBound - interval arithmetic for Lean 4

Stream: general

[Alejandro Radisic]

Hey all, sharing LeanBound

Tactics for proving bounds on transcendentals (exp/sin/cos) and polynomials using interval arithmetic. Similar spirit to CoqInterval.

def I01 : IntervalRat := ⟨0, 1, by norm_num⟩
-- Bound transcendentals
theorem exp_le_three : ∀ x ∈ I01, Real.exp x ≤ (3 : ℚ) := by interval_bound
theorem sin_le_one : ∀ x ∈ I01, Real.sin x ≤ (1 : ℚ) := by interval_bound

Also supports root existence/uniqueness proofs (via sign change and Newton contraction).

Core verified; some edge cases remain (see README).

https://github.com/alerad/leancert

Feedback welcome!