First Last

Chase Norman

PhD Student
chasen@cmu.edu

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:


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.

Chase Norman, Tesla Zhang, Anna Zhang, Cheng Zhang, Linxuan Ma, and Shubham Bhargava

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

Logic, Rationality, and Interaction (LORI) 2021

Voting Theory in the Lean Theorem ProverBibTeX

Wesley H. Holliday, Chase Norman, Eric Pacuit

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

PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory ConsistencyBibTeX

Chase Norman, Adwait Godbole, Yatin A. Manerkar

Conference on Automated Deduction (CADE) 2023

Program Synthesis in SaturationBibTeX

Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov

Contemporary Mathematics 2024

Impossibility theorems involving weakenings of expansion consistency and resoluteness in votingBibTeX

Wesley H. Holliday, Chase Norman, Eric Pacuit, Saam Zahedian