Understanding Proofs

About the Workshop

With AI proving theorems on our behalf a new frontier is creating human interpretable experiences and/or artifacts from those formal proofs. This workshop is for those that see formal proofs as encoding system knowledge in a compact, symbolic form. Here attendees will explore how to expose information that is today perhaps only accessible to formal methods subject matter experts. Future tools could also potentially reveal new ways to adapt existing proofs for novel challenges.

Organizers

• Byron Cook — Amazon|DARPA|University College London
• Andreas Podelski — University of Freiburg

Topics of Interest

Topics include, but are not limited to:

• Human understanding and interpretation of formal proofs
• Extracting, representing, and using knowledge encoded in proofs
• Proof explanation and exploration
• Interfaces and visualizations for interacting with formal proofs
• Proof abstraction, summarization, and decomposition
• Applications of understanding proofs, e.g., failure disgnosis and recovery

Call for Contributions

The workshop will feature invited talks and contributed presentations selected through an open call. We anticipate welcoming both research papers and shorter position papers, including preliminary results and emerging ideas.

Submission format, page limits will be announced. Submission link: Workshop Application.

Important Dates

Submission deadline: December 18, 2026
Notification of acceptance: January 31, 2027
Workshop date: April 10, 2027

Invited Speakers

To be announced.

Preliminary Program

Program still to be announced. Times are local to Copenhagen.

Registration and Venue

Workshop registration and venue information will be available through the ETAPS website.