Portfolio + Blog
Engineer and mathematician building at the boundary of neural networks and formal verification. Here you'll find projects, proof artifacts, and long-form writing on the space.
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.
Contact
Open to research collaborations, roles, and conversations about the future of provable AI.