2 Introduction

2.1 What is the formalization of mathematics?

Formalization of mathematics is the art of teaching a computer what a piece of mathematics means.

That is, it is the process of carefully writing down a mathematical statement typically in first order logic or higher order logic and then scrutinously justifying each step of the proof to a computer program that checks the validity of every step of the reasoning.

Typically one formalizes mathematics with the help of a proof assistant or interactive theorem prover, a piece of software which enables a human to write down mathematics and have the software verify the claims.

There exist many proof assistants, such examples are Lean, Isabelle, Coq, Metamath, etc.

For this project I have opted to use Lean due to its rapid growing mathematics library and its dependent type theory. I shall explain in more detail these last two reasons, but first I will comment on what Lean is.

What is Lean?

Lean is both a functional programming language and an interactive theorem prover that is being developed at Microsoft research and AWS by Leonardo de Moura and his team. It has been designed for both use in cutting-edge mathematics and the verification of software which is often essential to safety critical systems where correctness is of extreme TODO:

- Brief explanation of type theory and curry-howard isomorphism.

- Example of formal proof and comparison with informal proof.

2.2 Fermat’s Last Theorem

TODO:

-History of Fermat’s Equation

-Problem statements

-Developments in number theory that lead to the resolution of the conjecture.

2.3 Formalizing Fermat’s Last Theorem

Following the sequence of success stories ranging from the Liquid Tensor Experiment to the formalization of the Polynomial Freiman-Rusza conjecture.

Prof. Kevin Buzzard from Imperial College London has received a five-year grant that will allow him to lead the formalization of Fermat’s Last Theorem. This grant kicked in in October of 2024.

At the time of writing, since October of 2024, a digital blueprint has been set up to manage the project.

Alongside other infrastructure like the project dashboard, mathematicians around the world can claim tasks that are set by Prof. Kevin Buzzard and if in return a task is returned with a "sorry" free proof then one can claim the glory of having completed the task.

TODO:

- Current goal of the formalization

- Explain somewhat the modern approach and the highly sought after Modularity Lifting Theorem.

- My task: Classification of finite subgroups of \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\)

2.4 Classification of finite subgroups of the \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\)

TODO:

-Why are the finite subgroups of \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\) relevant to number theory: i.e: Automorphic forms, Galois representations, etc.

The primary concern of this project is to formalise Theorem 2.47 of [DTT] which states:

If \(H\) is finite subgroup of \(\operatorname{PGL}_2(\mathbb {C})\) then \(H\) is isomorphic to one of the following groups: the cyclic group \(C_n\) of order \(n\) (\(n \in \mathbb {Z}_{{\gt}0}\)), the dihedral group \(D_{2n}\) of order \(2n\) (\(n \in \mathbb {Z}_{{\gt}1}\)), \(A_4\), \(S_4\) or \(A_5\).
If \(H\) is a finite subgroup of \(\operatorname{PGL}_2(\bar{\mathbb {F}}_p)\) then one of the following holds:
1. \(H\) is conjugate to a subgroup of the upper triangular matrices;
2. \(H\) is conjugate to \(\operatorname{PGL}_2(\mathbb {F}_{\ell ^r})\) and \(\operatorname{PSL}_2(\mathbb {F}_{\ell ^{r}})\) for some \(r \in \mathbb {Z}_{{\gt}0}\);
3. \(H\) is isomorphic to \(A_4\), \(S_4\), \(A_5\) or the dihedral group \(D_{2r}\) of order \(2r\) for some \(r \in \mathbb {Z}_{{\gt}1}\) not divisible by \(\ell \)
Where \(\ell \) is assumed to be an odd prime.

By definition the Projective General Linear Group is:

\begin{equation} \operatorname{PGL}_n(F) = \operatorname{GL}_n(F) / (Z(\operatorname{GL}_n(F))) = \operatorname{GL}_n(F) / (F^\times I) \end{equation}

Similarly, the Projective Special Linear Group is:

\begin{equation} \operatorname{PSL}_n(F) = \operatorname{SL}_n(F) / (Z(\operatorname{SL}_n(F))) = \operatorname{SL}_n(F) / (\langle -I\rangle ) \end{equation}

Given we are working over an algebraically closed field \(F\), it turns out that for any \(n \in \mathbb {N}\), \(\operatorname{PGL}_n(F)\) is isomorphic to \(\operatorname{PSL}_n(F)\).

This isomorphism will be crucial as it will allow us to focus on classifying finite subgroups of \(SL_2(F)\) to classify the finite subgroups of \(\operatorname{PGL}_2(F)\).

The goal of the next chapter is to prove and formalize this result.