Formalization

Formalization projects in Lean 4.

Mathlib

Polygon geometry in Mathlib

Personal

Formalized Agent Foundations

More to come.

Lean-Eval

I have submitted solutions to the official Lean Eval for AI models. My submissions are housed in this repository. So far I have submitted solutions for 3 problems with GPT-5.5 in Codex.

About

More to come.