✧ Lean-Based Formal Verification Research

Conducting independent research in Lean-based formal verification, building an open-source math-reasoning model using Lean's formal kernel.

Curated high-quality training data pairing natural language mathematical reasoning with formal Lean proofs.

Developed a self-supervised RLAIF (Reinforcement Learning from AI Feedback) pipeline to translate natural language reasoning into formally verified proofs.

Working toward bridging the gap between informal mathematical intuition and machine-checkable formal verification.