In Chapter 1, we will introduce L2 -Betti numbers after covering the preliminaries for this definition. We will also show an algebraic characterisation of L2 -Betti numbers:
For a group G, all L2 -Betti numbers arising from G are given as dimRG ker(·A) for some self-adjoint A ∈ Mn×n(ZG) (see Section 1.2.4). In Section 1.3, we will cover Atiyah’s conjecture and Lück’s approximation theorem.
Chapter 2 is dedicated to the introduction of computability concepts. After a ‘naive’ introduction into this subject, we will define different computability classes such as EC (effectively computable), LC (left-computable) and RC (right-computable). We will then take a look at some results on right-computability of topological invariants (Section 2.3).
The main part of this thesis is Chapter 3. We will start with a survey on some known computability results on L2 -Betti numbers (Section 3.1). We will then discuss right-, left- and effective computability of L2 -Betti numbers under different assumptions.
Finally, in Chapter 4, we will discuss an implementation of some of the main results in the Lean Theorem Prover. This formally verifies some of these results. The .lean files used for this can be found on a git repository online. More information on how to install these files can be found in Section 4.2.

In Kapitel 1 führen wir L2-Betti-Zahlen ein, nachdem wir zunächst einige Grundlagen behandeln. Wir zeigen auch eine algebraische Charakterisierung von L2-Betti-Zahlen: Ist G eine Gruppe, dann sind alle L2-Betti-Zahlen durch dimRG ker(·A) für ein selbst-adjungiertes A ∈ Mn×n(ZG) gegeben (siehe Abschnitt 1.2.4). In Abschnitt 1.3 behandeln wir Atiyahs Vermutung und den Lück'schen Approximationssatz.
Kapitel 2 ist der Einführung in die Berechenbarkeit gewidmet. Nach einer `naiven' Einführung definieren wir verschiedene Berechenbarkeitsklassen wie EC (effektiv berechenbar), LC (links-berechenbar) und RC (rechts-berechenbar). Wir behandeln Resultate zur Berechenbarkeit topologischer Invarianten (Abschnitt 2.3).
Der Hauptteil (Kapitel 3) startet mit einem Diskurs bekannter Berechenbarkeitsresultate zu L2-Betti-Zahlen (Abschnitt 3.1). Anschließend behandeln wir die effektive, Links- und Rechts-Berechenbarkeit von L2-Betti-Zahlen unter bestimmten Voraussetzungen.
Abschließend wird in Kapitel 4 eine Implementierung im Lean Theorem Prover behandelt. Diese verifiziert formal einige der Resultate. Die .lean-Dateien können in einem git repository gefunden werden (online, siehe Abschnitt 4.2).