Interactive theorem prover make it possible to conduct formal proofs, e.g. about mathematics or program verification, with the help of a computer. The computer does not only check the correctness of the final proof but also assists in the process of writing it. So far, the theorem prover Lean does so by interactively displaying the current proof goal. For more specific applications there are additional so-called widgets which offer graphical support for writing certain proofs. For example, here is a widget which assists at solving a sudoku puzzle or a Rubik's cube:
Quelle: Markus Himmel, https://github.com/TwoFX/sudoku
Quelle: Kendall Frey, https://github.com/kendfrey/rubiks-cube-group
In the mathematical field of category theory, more precisely in the area of monoidal categories, string diagrams are used as a graphical representation of mathematical objects, to make proofs more intuitive:
Quelle: Peter Selinger, A Survey of Graphical Languages for Monoidal Categories
The goal of this thesis project is to build a VS Code Widget for Lean, which displays morphisms in certain classes of monoidal categories and provides the means of manipulating them.
Prerequisits
- Knowledge of abstract algebra
- Experience with theorem provers or dependent types is not necessary
Advisors
| Scientific Staff |
|---|
| Dr. Jakob von Raumer |