• Formalizing Maths and Developing Automation in Lisa

Are you interested in learning about foundations of mathematics? Theorem proving in a proof assistant? Decision procedures?
In this project, you will formalize a mathematical theory, or develop a proof-producing tactic in the Lisa proof assistant and, if you desire, contribute to its standard library.

Lisa is a proof assistant based on set theory and developed in Scala. Familiarity with mathematical logic, basic set theory and/or Scala can help you to progress faster, but you are also welcome if you don't have any experience with either and wish to learn. Regarding formalization of a mathematical theory, good topic examples are:

• Arithmetic (Natural numbers, Integers, Rationals, Reals, ...)
• Algebra (Groups, Rings, Fields, ...)
• Combinatorics (Graph Theory, ...)
• Topology (Non-metric)
• Category Theory

The list is non-exhaustive; other topics may be suitable too, but as a rule of thumb any topic requiring analysis or much use of real numbers might be difficult. Alternatively or in conjunction, depending on the scope of the project, you might develop proof-producing decision procedures (i.e. tactics). Doing so, you will have both practical and theoretical concerns, including runtime in practice, features, theoretic complexity, completeness, etc. Here are some possibilities (non-exhaustive):

• Solver for linear integer arithmetic (Presburger arithmetic)
• Solver for first order logic (Superposition, Resolution, ...)
• Proof transfer from an external automated theorem prover

These projects are suitable for Bachelor Semester Projects, Master Semester Projects and Master thesis

• Lemma Search with Orthologic

The libraries of proof assistants quickly become too large to search manually. Users need to find specific lemmas all the time, but often don't know the name of the lemma or if it even exists. To solve this problem, proof assistants offer more or less sophisticated search tools. The simplest search for textual representations of a desired lemma, and more advanced ones can look for patterns such as "0 * _ = 0". Yet, it is frequent that a lemma exists but is slightly different from what the user searched, for example "n * 0 = 0" (This example is for illustration. In practice, a theorem prover is likely to contain both 0 * n = 0 and n * 0 = 0) Can we find lemmas, with patterns, modulo laws or orthologic or variants? In the example above, we could find that the pattern matches modulo commutativity.

This project mixes theoretical computer science and engineering. You will design algorithms, related to caching and matching modulo theories, and implement them, e.g. in Lean or Lisa, for use by the community. This project is suitable for Master Semester Projects and Master Theses

• Using SAT solvers to solve Jigsaw Puzzles

A solution to a (generalized) jigsaw puzzle should be difficult to find, but easy to check. Can SAT solvers help solve this problem? This project is inspired by this video from the excellent Matt Parker on his Stand-up Maths YouTube channel.

In a traditional jigsaw puzzle, all the "in" bits are distinct, so that it can only fit a single "out" bit. On the other extreme, if all the bits are the same, the puzzle will have many solutions. The holy grail is to find a set of pieces, for a fixed-size puzzle, which admits exactly two solutions. A useful component for this problem is a jigsaw checker: Given a set of pieces, how many solutions does it have? The project will contain a mix of literature review, theoretic research and implementation.

• What is the complexity class of the problem and variants of the problem? (for example, does it admit a reduction to and from #SAT?)
• Study of state-of-the-art SAT solvers and techniques to encode optimization problems
• Design and implement a jigsaw checker, using a SAT solver as oracle, which outperforms existing implementations
• Using it, find a set of pieces with exactly two solutions which don't share an edge

This project is suitable for Bachelor Semester Projects (if you already have some familiarity with the topic) and Master Semester Projects

• Create Lisa proof files from Lean files and blueprint

Existing theorem provers have huge libraries, the result of countless hours of work from countless people. While proof assistants differ in foundations, available tactics and general approach, at a higher level, theorems and the development of theories still follow similar lines: the same key lemmas are required to prove a desired theorem. A lot of work in formalization is laying out the general structure of a development, before filling any proof. Some tools exist to help with these tasks, for example blueprints in Lean.

Is it possible to transfer and reuse this structure across proof assistants? The goal of this project is to implement a tool that will create template Lisa files to guide the development of mathematical theories. The approach could be AI based, deterministic, or a mix of both. Large language models are already somewhat capable of translating code from one language to another, and translating from one proof assistant to another is largely similar, except for the available training data. Deterministically, it should be possible to establish a dependency graph of lemmas, definitions and theorems to implement a skeleton file, though differences in syntax and foundation may make restating statements and definitions non-trivial even without proofs. Even with placeholders to manually fill, it would be a novel and useful tool.

This project is suitable for Master Semester Projects and Master Theses