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.
AERO, CSE, ROB
Funding: $30K (2023)
Goal: An open source software tool for interactively generating formal proofs, which will be evaluated with a human subjects study involving graduate students in the CoE
Token Investors: Cyrus Omar and Jean-Baptiste Jeannin
Project ID: 1111