Interactive theorem provers make it possible to conduct formal proofs about mathematics or program verification with the help of a computer, i.e. the computer does not only check the correctness of the final proof but also assists in the process of writing it.
An essential part of proving is to use previously established equalities to rewrite other terms. In Lean, this currently happens via the application of so called tactics. Even though the state of the proof goal can be inspected after each tactic application, the selection of the subterms in which the rewriting is supposed to happen is a bit unwieldy.
The goal of the thesis project is to equip Lean's proof goal view with the ability to interactively select and apply subterms and rewriting lemmas.
The code will be written completely in the language Lean itself.
Prerequisits
- Knowledge of functional programming
- Experience with theorem provers or dependent types is not necessary
Advisors
