Interactively Deriving Formal Proofs

In science and engineering, many mathematical derivations are still performed by hand, on whiteboards or typeset with LaTeX or Word. The correctness of these derivations are then checked by hand. Modern theorem provers enable computer-checked proofs, but they impose an idiosyncratic syntax and workflow that is unfamiliar to scientists and engineers. We plan to develop a tool that allows scientists and engineers to interactively build computer-checkable derivations while retaining a natural interaction style familiar to scientists and engineers. The output of the tool will be both a formal, computer-checkable proof (written in a theorem prover like Coq or Agda) and typeset output suitable for incorporation into publications (using LaTeX). We will start with simple algebraic manipulations, then target a number of more specialized scientific and engineering domains with more specialized visual notations. This project combines the PIs’ expertise in formal methods and user interface design.

People

Project ID: 1111