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.