Doctoral Thesis Oral Defense - Joshua Clune

About this event

Speaker: JOSHUA CLUNE, Ph.D. Candidate, Computer Science Department, Carnegie Mellon University

Talk Title: Leveraging Automated Theorem Provers for Lean Proof Automation

Automated and interactive theorem provers are closely related technologies that complement each other well. Interactive theorem provers offer expressive proof languages with strong correctness guarantees, and automated theorem provers offer fast and convenient automation for generating proofs. By using automated theorem provers to enhance the proof automation in interactive theorem provers such as Lean, it is possible to simultaneously benefit from the convenience of automated theorem proving and the trustworthiness of interactive theorem proving.

This thesis presents four projects, each of which seeks to develop and improve Lean proof automation either by leveraging automated theorem provers directly or by providing the infrastructure to do so more effectively. The first is a proof-producing automated theorem prover capable of generating proofs directly in Lean. The second is a hint-based approach to SMT proof reconstruction. The third is an LM-based premise selection system. The final project is a domain-general end-to-end hammer for Lean. Each of these projects are carefully evaluated against contemporary alternatives and shown to improve the efficacy of Lean's proof automation.

Thesis Committee:

Jeremy Avigad (Chair)

Marijn Heule

Bryan Parno

Haniel Barbosa (Universidade Federal de Minas Gerais)

In-person & Zoom