Deterministic, auditable Lean 4 + mathlib reasoning instrument (not an oracle): contracts, assumption surfacing, reduction scaffolds, dashboard + PDF reports.
theorem-proving proof-assistant deterministic formal-verification mathlib lean4 research-tooling auditibility
-
Updated
Dec 30, 2025 - Lean