• 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.

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, incuding runtime in practice, features, theoretic complexity, completeness, etc. Here are some possibility (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 becomes too large to manually 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 problems, proof assistants offer more or less sofisticated search tools. The simplest search for textual representations of a desired lemma, and more advanced one can look for paterns such as "0 * _ = 0". Yet, it is freequent 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 contains both 0 * n = 0 and n * 0 = 0) Can we find lemmas, with paterns, modulo laws or orthologic or variants? In the example above, we could find that the patern 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 from this video from the excellent Matt Parker on his Stand-up Maths YouTube channel.

In a traditional jigsaw puzzle, every all the "in" bits are distincts, 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 solution. The holy grail is to find a set of pieces, for a fixed sized 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 literaturee 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 an 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 and 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 persons. While proof assistants diffeer 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 aree 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 this 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 templates 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, if for the available training data. Deterministically, it should be possible to establish a dependency graph of lemma, definitions and theorems to implement a skeleton file, though differences in syntax and foundation may make restating statement 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