Projects

Formalization of Ramsey Theory

formal_ramsey

A Lean 4 formalization of finite Ramsey theory, proving exact values for several small Ramsey numbers and related van der Waerden numbers. We also give Lean-verified SAT encodings for Ramsey numbers and demonstrate the use of LRAT proofs in Lean. This is the project behind our CICM 2024 paper, “Formalizing Finite Ramsey Theory in Lean 4,” and we plan to submit it to mathlib as a reusable library for Ramsey-theoretic results.

RamseyLemmas

Formalizing results in Ramsey theory due to Graver and Yackel, which were used in the SAT certification of the Ramsey numbers R(3,8) and R(3,9) by Zhengyu Li.

Verifying Parsers

cedar-spec

Cedar is AWS’s open-source authorization policy language and the engine behind Amazon Verified Permissions. This project formally verifies Cedar’s extension parsers — for decimals, durations, datetimes, and IP addresses — with all correctness theorems machine-checked in Lean 4. Part of my internship with the Amazon Automated Reasoning group.

triptych

A Lean 4 grammar-to-parser compiler for flat, non-recursive string formats. From a single grammar definition, triptych produces three coordinated outputs — a human-readable specification, a verified executable parser, and machine-checked correctness theorems — relying only on standard Lean axioms.

Lean Tools

LeanGraphMaker

Widgets and tactics that let you generate, manipulate, and visualize graphs and their substructures on a canvas embedded in the Lean 4 Infoview. Visual data is sent back to the Lean workspace via RPC and parsed into formal terms. This is the project behind our HATRA 2026 paper, “Just Draw It.”

Imandra-Lean

Work from my internship at Imandra: extending Imandra-Geo, a solver for nonlinear real arithmetic, to generate proof certificates in Lean, plus custom Lean tactics (via metaprogramming) that normalize nonlinear real arithmetic expressions and translate Lean syntax into Imandra-Geo input.