I am a third 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:

One Unified Robust Approach 􀅼

Learning from Experience 􀅼

Metatheoretic Reasoning 􀅼

Executing Concrete Strategy 􀅼

Maintaining and Creating Abstraction Barriers 􀅼

Canonical

Automated Theorem Proving for General Mathematics.

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

Install Canonical for Lean 4 with the following in your lakefile.toml:

[[require]]
name = "Canonical"
scope = "chasenorman"

􀐅

Lean, Mean, Machine.

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