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
Jan 9, 2026 - Lean