Symbolic computation appears frequently in mathematical proofs, as well as in sciences and engineering. While proof assistants can be used to formally verify symbolic computation, such a task currently requires a thorough understanding of the proof assistant and its mathematical library. HolPy is a new proof assistant implemented in Python, intended to explore both better proof automation and new ways for user interaction. In this talk, I will begin by introducing the basic ideas of HolPy, then show how it can be used to verify symbolic computation using an user interface that is very much like computer algebra systems, together with a point-and-click style of interaction for performing and checking calculation steps.
Copyright. All Rights Reserved.