Projects
Formal reasoning systems, from manual proof engineering to fully automated library generation.
An AI-assisted mathematical formalization engine for Lean 4. Given an underdeveloped area of Mathlib, it decomposes it into a structured blueprint and proves every entry automatically — producing a complete, verified library with zero sorry and zero axiom.
Formally verified theorems in Lean 4 demonstrating structured inductive reasoning on natural numbers. Manual tactic proofs from foundational algebra through division algorithm uniqueness — no automation shortcuts.