Doctoral Thesis Proposal - Joshua Clune

— 11:30am

Location:
4405 & Zoom - Gates and Hillman Centers

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

Leveraging Automated Theorem Provers for Lean Proof Automation

This proposal discusses work that builds towards the creation of a hammer for the Lean interactive theorem prover. Said work includes the development of a proof-producing superposition theorem prover for Lean, a tool which interfaces with the cvc5 SMT solver to produce self-contained Lean proof scripts, and a neural premise selection system. The proposal culminates in the description of a preliminary hammer for Lean along with discussion of how to refine and improve it into a more powerful and robust tool.

Thesis Committee:

Jeremy Avigad (Chair)
Marijn Heule
Bryan Parno
Haniel Barbosa (Universidade Federal de Minas Gerais)

In-person and Zoom

Contact
Matt Stewart

Add event to Google
Add event to iCal