I am a second year Computer Science PhD student at Carnegie Mellon University
advised by Prof. Jeremy Avigad in the Hoskinson Center.
My office is 9002 Gates and Hillman Centers.
I was an attendee of the 9th and 11th Heidelberg Laureate Forums.
I am a fellow of the National Science Foundation (NSF) **Graduate Research Fellowships Program**.
I completed my undergraduate degrees in Mathematics and Computer Science with a minor in Music at UC Berkeley.

If what they were working on was not important and was not likely to lead to important things, then why were they working on them?

— Richard Hamming

To me, the most important problem is Automated Theorem Proving (ATP).
Proving arbitrary theorems from mathematics is definitionally **the hardest problem** in computer science.
Solving this one problem would solve **all formal problems at once**.
The following diagram from descriptive complexity theory shows complete problems for increasingly difficult complexity classes:

**ELEMENTARY** — HoL

**PSPACE** — TQBF, IPL

**NP** — SAT

**P** — HornSAT

**
Recognizable / Semi-Decidable / Turing Complete** —

Dependent Type Theory (General ATP)

ATP is the **only formal problem with no known algorithm** matching human performance.
Such an algorithm has applications in formal verification, mathematical discovery, generative design, and **all manner of fields** with elements of deductive reasoning or logic.
My goal is to build a human-level automated theorem prover.

My most important philosophy is first-principles thinking.
I start from the end goal and work my way back to the solution.
In ATP, this means designing a maximally simple formal language for mathematics and building in human-inspired general reasoning capabilities from the start.
This is my research project **Canonical**.

My approach to ATP is unique in a few key ways:

## Canonical

Automated Theorem Proving for General Mathematics.

Canonical exhaustively searches for proofs of any mathematical statement in dependent type theory.

#### The Only Tactic that Always Applies.

#### Real, Human-Readable Proofs.

Canonical writes proof terms **directly as Lean code**, visible to you.

Canonical adds **no compile time** to your project after generation.

Your collaborators and users do **not need to install** Canonical.

#### Solves the “Last Mile” of Formalization.

A proof term has a tree structure, so most of the work is near the leaves.

Canonical solves low-depth problems.

The “Last Mile” Problem contributes to the **10-20x** overhead in formalizing pen and paper proofs.
Canonical can help close this gap.

#### A Tour de “Brute Force.”

Sound and Complete inhabitation for Dependent Type Theory.

Canonical executes millions of tactics* every second, in **parallel**, and optimized with intelligent heuristics and pruning.

Canonical searches only **type-correct partial terms** and only **canonical forms**.

Canonical can fill function arguments **out of order**, to leverage unification.

Canonical is **goal-directed**, only making relevant inferences.

* where a tactic is defined as an elementary intro or apply

## Publications

Architectural Support for Programming Languages and Operating Systems (ASPLOS) 2023

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency BibTeXContemporary Mathematics 2024

Impossibility theorems involving weakenings of expansion consistency and resoluteness in voting BibTeX