Verifying Symbolic Computation in the HolPy Theorem Prover - IPAM at UCLA

Explore a conference talk on verifying symbolic computation using the HolPy theorem prover. Delve into the basics of HolPy, a new proof assistant implemented in Python, and discover its potential for improved proof automation and user interaction. Learn how HolPy can be utilized to verify symbolic computation through a user interface similar to computer algebra systems, featuring point-and-click interaction for performing and checking calculation steps. Examine examples of verifying definite integrals, integration by parts, and trigonometric identities. Gain insights into proof reconstruction, the overall architecture of HolPy, and its limitations. Investigate extensions, new rules, and future work in this field. Compare HolPy's approach with traditional computer algebra systems and understand the division of labor in symbolic computation verification.

Intro
Outline
Introduction to Holly
Python API for proof automation
Python API example
Verification of definite integrals: motivation
Basic idea
Example: integration by parts
Example: trigonometric identity
Proof reconstruction
Summary: overall architecture
Example #1
Example #2
Limitations
Extensions
New rules
Examples
Example #4
Summary: division of labor
Summary: comparison with CAS
Future work