Lean4 - How the theorem prover works and why it's the new competitive edge in AI
Large language models struggle with reliability and hallucinations. This article explores how Lean4, an interactive theorem prover, acts as a truth kernel to mathematically verify AI outputs, creating a new standard for deterministic and safe AI.
Nov 23, 2025
Math Thesis Defense - Lean4 Machine Assisted Proof Framework for Chip Firing Game & Graphical Riemann-Roch
Mathematics Thesis Defense Talk and Q&A for Dhyey Mavani's work with Professor Nathan Pflueger.
Apr 15, 2025
Mathematics Honors Thesis at Amherst College (Summa cum laude)
We formalize chip-firing games and the Riemann-Roch theorem on graphs, enabling structured proofs and machine-driven research exploration.
Apr 15, 2025
Lean4 Machine Assisted Proof Framework for Chip Firing Games & Graphical Riemann-Roch
We formalize chip-firing games and the Riemann-Roch theorem on graphs, enabling structured proofs and machine-driven research exploration.
Apr 15, 2025