## Authors: Alexandra Mendes and Joao F. Ferreira

## Paper Information

Title: | Towards Verified Handwritten Calculational Proofs (short paper) |

Authors: | Alexandra Mendes and Joao F. Ferreira |

Proceedings: | ITP Papers |

Editors: | Jeremy Avigad and Assia Mahboubi |

Keywords: | handwritten mathematics, interactive theorem proving, mathematical proof, calculational method, handwriting, IDE |

Abstract: | ABSTRACT. Despite great advances in computer-assisted proof systems, writing formal proofs using a traditional computer is still challenging due to mouse-and-keyboard interaction. This leads to scientists often resorting to pen and paper to write their proofs. However, when handwriting a proof, there is no formal guarantee that the proof is correct. In this paper we address this issue and present the initial steps towards a system that allows users to handwrite proofs using a pen-based device and that communicates with an external theorem prover to support the users throughout the proof writing process. We focus on calculational proofs, whereby a theorem is proved by a chain of formulae, each transformed in some way into the next. We present the implementation of a proof-of-concept prototype that can formally verify handwritten calculational proofs without the need to learn the specific syntax of theorem provers. |

Pages: | 9 |

Talk: | Jul 11 16:40 (Session 67C) |

Paper: |