Abschlussarbeiten

The Lean theorem prover is built on a fairly minimal core type theory. By design, Lean itself is not particularly trustworthy (e.g. it allows users to circumvent its type system in ways that are hard to detect), but it can export finished proofs, which are terms of the core type theory. These can then be checked by small, trustworthy third-party checkers (1, 2, 3).

The aim of this project is to build one such checker (though we may limit the scope to a subset of the core type theory). To do so, you'll have to familiarise yourself with the rules of the core type theory and then define its abstract syntax and write a parser and typechecker.

Familiarity with basic compilation techniques (parsing, abstract syntax, typechecking) is required. Experience with dependent type theories would be very helpful. The project is suitable for a master or strong bachelor student.

The Lean theorem prover has a very flexible parsing mechanism which allows us to embed other languages into it. In this project, we'd like to use this mechanism to embed intensional or extensional Martin-Löf type theory. This means you'll have to define the abstract syntax and type system of this type theory in Lean and write a parser type checker for it. (We aim to use the embedded type theory to simplify proofs about its categorical models.)

A solid command of functional programming is required, as is familiarity with basic compilation techniques (parsing, abstract syntax, typechecking). Experience using theorem provers based on dependent type theory (e.g. Agda, Coq, Lean) would be very helpful. The project is suitable for a master or strong bachelor student.

In the Lean theorem prover, some tasks, such as proving the continuity of a function or a linear inequality, can be automated by using some sort of specific strategy. For example, the `continuity` tactic uses a general theorem prover restricted to some set of lemmas that concern continuity to complete a goal.

This project aims to improve existing specialised tactics available in Mathlib or create new ones that would solve particular types of goals.

To tackle this project, you will have to familiarise yourself with some of the metaprogramming APIs of Lean, for which a solid command of functional programming, including monads, is required. Experience with theorem provers based on dependent type theory (e.g. Agda, Coq, Lean) would be helpful.

Contact persons:

• Dr. Martin Desharnais-Schäfer (Isabelle/HOL)
• Dr. Michael Kirsten (Isabelle/HOL)
• Yiming Xu, PhD (Lean, HOL4)
• Xavier Généreux (Lean)
• Luca Maio (Lean)
• Balazs Toth (Isabelle/HOL)
• Alexandra Graß (Isabelle/HOL)

This type of thesis aims to define and then prove some interesting properties about a mathematical concept, system, structure, or implementation, using Isabelle [1], Lean [2], or HOL4 [3]. There exists a wide variety of possible formalization projects; you may either come to us with an idea of your own, or we look for one in a field that interests you.

For a project like this, prior experience with Isabelle, Lean, or HOL4 (or another proof assistant like Coq or Agda) is very helpful but not strictly required if you are willing to learn to use them in the process. For Master's level, due to the probable scope of the project, not having prior experience might prove to be challenging, though.
Resources: Lean 4 learning material, Isabelle Tutorial, Concrete Semantics with Isabelle/HOL, Functional Data Structures and Algorithms, HOL4 Tutorial and Documentation.

[1] https://isabelle.in.tum.de/
[2] https://lean-lang.org/
[3] https://hol-theorem-prover.org/

Some interesting projects:

Verify Your Favourite Voting Rule:

A voting rule is an algorithm that calculates a collective election result from a set of individual preferences. There are numerous different types of voting rules, both in academia and in elections in practice. However, since Kenneth J. Arrow described the general impossibility theorem in 1950, it has been clear that it is not possible to derive a result from the wishes of a society without abandoning at least certain desired principles. In real-world voting rules, attempts are often made to fulfill a relatively large number of these principles without causing any particular (negative) effects. For example, due to such a negative effect, the voting rule for determining the German Bundestag in 2008 was ruled unconstitutional. The reason for this was negative vote weights, which meant that some votes carried more weight than others. Here, we develop methods to synthesize provenly correct voting rules with regard to these and similar properties (generally referred to as social choice properties) using the Isabelle/HOL theorem prover. As part of a thesis, it would be interesting to apply this technique to other, more complex or exotic voting rules, e.g., used in real life and, on the one hand, to examine the extent to which the method fulfills the claimed properties and, on the other hand, to evaluate the scalability of the verification techniques. In collaboration with your supervisor, you can choose an exciting voting rule that is supposed to fulfill certain social choice properties.

The aim of this project is to formalize the theory of the groupoid model of homotopy type theory, and then employ Lean meta-programming to implement a theorem prover for HoTT0 (a fragment of HoTT with univalence for sets) using our formalization. This project will be co-supervised by the team based at Carnegie Mellon University (CMU). Students are supposed to work on issues listed here and make a contribution to this git repository.

These projects aim at formalizing basic theorems from the field of propositional proof complexity and their proofs in an interactive proof assistant like Isabelle or Lean. Some example results for a start could be:

The exponential lower bound on the length of resolution proofs of the pigeonhole principle.

The size-width trade-off for resolution proofs.

Separations between various restricted forms of resolution proofs.

Existing formalizations of the concepts of resolution and other proof systems may be used as a basis.

A CNF-formula is an instance of (k,s)-SAT, if every clause has exactly k literals, and every variable occurs at most s times. It is known that for every k, there is an s=s(k) such that (k,s)-SAT is trivial (all such formulas are satisfiable), but (k,s+1)-SAT is NP-complete. Asymptotically, the value of s(k) is known, but for small values of k, the exact values are unknown. Due to the dichotomy, in order to improve the known upper bounds, it suffices to find a single unsatisfiable formula for certain values of k and s. The task is to experiment with machine learning methods to find such unsatisfiable formulas.

First experiments in this direction have already been undertaken. For further work on this topic a firm knowledge of machine learning techniques is required.

Lifting is a technique to produce hard instances of CNF formulas from easier ones. In a recent paper [1], a lower bound for proofs of certain lifted formulas in the regular resolution proof system was shown. For these formulas, upper bounds in a stronger proof systems related to clause learning [2] should be derived.

[1] Vinyals, Elffers, Johannsen, Nordström, "Simplified and Improved Separations between Regular and General Resolution by Lifting", SAT 2020

[2] Buss, Hoffmann, Johannsen, "Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL-Algorithms with Clause Learning", LMCS 4, 2008.