main.tex

\documentclass[fleqn, leqno, a4paper, openright, oneside, 10pt]{memoir}
%\documentclass[10pt]{memoir}

%\newlength{\pagew}
%\newlength{\pageh}
%%\setlength{\pagew}{210mm}
%%\setlength{\pageh}{297mm}
%\setlength{\pagew}{125mm}
%\setlength{\pageh}{201mm}
%
%\setlength{\headheight}{20pt}
%\setlength{\headsep}{10pt}
%\setlength{\footskip}{20pt}
%
%% \setlength{\headheight}{0pt}
%% \setlength{\headsep}{40pt}
%% \setlength{\footskip}{25pt}
%% \setlength{\pagew}{125mm}
%% \setlength{\pageh}{205mm}
%
%\setstocksize{\pageh}{\pagew}
%\settrimmedsize{\pageh}{\pagew}{*}
%\settypeblocksize{170mm}{110mm}{*}
%\setlrmargins{*}{*}{1}
%\setulmargins{*}{*}{1}
%\setmarginnotes{0cm}{0cm}{0cm}
%\checkandfixthelayout

%\usepackage[pass, showframe]{geometry}

\usepackage[french]{babel}

% \usepackage{tgpagella}
% \usepackage[T1]{fontenc}

\usepackage{mathtools}
\usepackage[mathscr]{eucal}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{physics}
% \usepackage{newpxmath}

\usepackage[math-style=ISO, bold-style=ISO]{unicode-math}

%\setmainfont{TeX Gyre Pagella}
%\setmathfont{TeX Gyre Pagella Math}

%\setmainfont{Junicode}[Language=Turkish]
\setmainfont{Junicode SmExp}[
Language=French,
BoldFont = Junicode SmExp Bold,
ItalicFont = Junicode SmExp Italic,
BoldItalicFont = Junicode SmExp Bold Italic
]
%\setmainfont[Language=French]{Andada Pro}
%\setmainfont{Cooper}[
%BoldFont = Cooper-Medium.ttf,
%ItalicFont = Cooper-Italic.ttf,
%BoldItalicFont = Cooper-MediumItalic.ttf
%]
%\setmainfont{EB Garamond}

\setmathfont{Garamond-Math.otf}[StylisticSet={7,9}, Scale=MatchUppercase]
%\setmathfont[range=it]{Junicode Italic}
\setmathfont[range=it]{Junicode SmExp Italic}
\setmathrm{Garamond Libre}
%\setmathfont{STIX Two Math}[Scale=MatchUppercase]

%\setmainfont{KPRoman}
%\setmathfont{KPMath}

%\setmainfont{STIX Two Text}
%\setmathfont{STIX Two Math}

\setmonofont[Scale=MatchLowercase]{Iosvmata}

\usepackage{microtype}

%\setSingleSpace{1.15}
%\SingleSpacing

\usepackage{caption}
%\captionsetup{justification=raggedright,singlelinecheck=false}
\setlength{\mathindent}{1em}

\cftpagenumbersoff{chapter}

% Put figures at the end of the document
\usepackage[nomarkers, figuresonly]{endfloat}

% \usepackage[no-math]{fontspec}
% \setmainfont{EB Garamond}
% \setmonofont[Scale=MatchLowercase]{JetBrains Mono}
%
% \usepackage{microtype}
%
% \usepackage{mathspec}
% \setmathrm{EB Garamond}
% \setmathfont(Digits,Greek,Latin){EB Garamond}
%
% \makeatletter % undo the wrong changes made by mathspec
% \let\RequirePackage\original@RequirePackage
% \let\usepackage\RequirePackage
% \makeatother

\usepackage{graphicx}
\usepackage{rotating}
\usepackage{svg}
\usepackage{minted}

\definecolor{bg}{rgb}{0.95,0.95,0.95}
%\newmintinline[lean]{lean}{bgcolor=bg}
%\newminted[leancode]{lean}{bgcolor=bg}
\newmintinline[lean]{text}{bgcolor=bg}
\newminted[leancode]{text}{bgcolor=bg}
\usemintedstyle{tango}

\usepackage{float}
\usepackage{enumitem}
\usepackage{tabto}

\makeatletter
\newcommand\iraggedright{%
  \let\\\@centercr\@rightskip\@flushglue \rightskip\@rightskip
  \leftskip\z@skip}
\makeatother

\usepackage{lipsum}
\usepackage{dirtytalk}

\usepackage{pst-solides3d}
\psset
{
  lightsrc=viewpoint,
  Decran=30,
  solidmemory,
}

\usepackage{tikz}
\usetikzlibrary{intersections}

\usetikzlibrary{external}
\tikzexternalize[prefix=ext/]

% \usepackage{comment}
% \excludecomment{figure}
% \excludecomment{sidewaysfigure}
% \let\endfigure\relax
% \let\endsidewaysfigure\relax

\usepackage[
backend=biber,
style=alphabetic
]{biblatex}
\addbibresource{main.bib}

\usepackage{csquotes}

\usepackage[
unicode,
%colorlinks
]{hyperref}

\usepackage{cleveref}

\counterwithout{figure}{chapter}
\maxtocdepth{subsection}
\setsecnumdepth{section}
\renewcommand\thesection{\arabic{section}}

% Remove the word "Chapter n" from chapter heading, and adjust spacing.
\makeatletter
\renewcommand\printchaptername{}
\renewcommand\printchapternum{}
\renewcommand\chaptitlefont{\bfseries\scshape\Large}
\renewcommand\secheadstyle{\bfseries\large}
\renewcommand\beforechapskip{0cm}
\renewcommand\midchapskip{0pt}
\renewcommand\afterchapskip{1.8ex}
\makeatother

\newtheorem{thm}{Théorème}
\newtheorem{prop}{Proposition}
\theoremstyle{definition}
\newtheorem{defn}{Définition}
\theoremstyle{remark}
\newtheorem{exm}{Exemple}

% Unbutton the vector space from its origin.
\newcommand{\unbutton}[1][.7]{\mathbin{\hspace{1pt}\vcenter{\hbox{\scalebox{#1}{$\bullet$}}}}}

% Definitional equal.
\newcommand{\defeq}{\vcentcolon=}

% Explicit set and set comprehension.
\newcommand{\set}[1]{\{ #1 \}}
\newcommand{\setcomp}[2]{\set{ #1 \,|\, #2 }}

% Projectivization.
\newcommand{\proj}{\symbfscr{P}}

% Disjoint union.
\newcommand{\discup}{\mathop{\dot{\cup}}}

% Partial map.
\newcommand*{\DashedArrow}[1][]{\mathbin{\tikz
    [baseline=-0.25ex,-latex, dashed,#1] \draw [#1] (0pt,0.5ex) --
    (1.3em,0.5ex);}}%
\newcommand{\partialto}{\DashedArrow[->,dash pattern=on 4pt off 2pt]}

% Kernel and domain.
\DeclareMathOperator{\kernel}{Ker}
\DeclareMathOperator{\domain}{Dom}

% Common sets
\newcommand{\R}{\mathbf{R}}

\begin{document}
\frontmatter
\pagestyle{empty}
\pagenumbering{gobble}
\begin{center}
  \vspace*{\fill}
  % {%
  % \setlength{\fboxsep}{0pt}%
  % \fbox{\includesvg[width=3cm]{logo.svg}}%
  % }
  \includesvg[width=2.5cm]{logo.svg}

  \vspace{1cm}
  \large{\textbf{PROJET DE FIN D'ÉTUDES}}

  \vspace{0.5cm}
  {\small pour obtenir le diplôme de}

  \vspace{0.5cm}
  l'\textsc{\textbf{Université Galatasaray}}

  {\small Spécialité : \textbf{Mathématiques}}

  \vspace{0.75cm}
  {\Large\textbf{Formalisation du théorème de Desargues en Lean}}

  \vspace{0.75cm}
  Préparé par \textbf{Abdullah Uyu}

  Résponsable : \textbf{Can Ozan Oğuz}

  \vspace*{\fill}
  \textit{Juin 2024}
  \vspace*{\fill}
\end{center}
\iraggedright
\raggedbottom
\clearpage
\null{}
\vfill{}
Ce document est composé avec \texttt{LuaTeX} dans Junicode pour le
corps du texte, Garamond Math et Junicode pour les mathématiques et Iosvmata
pour le code source, tous en 10pt.

Le code source de la formalisation, ce document et le schéma de preuve
peuvent être trouvés dans \url{https://github.com/oneofvalts}.
\chapter*{Remerciments}
Tout d'abord, je tiens à remercier mon professeur, Can Ozan, pour
l'attention et le soin qu'il a apportés à mon étude. Il a non seulement
suivi les développements de mon étude, mais il a également appris à mes
côtés pour mieux me guider. J'étais toujours enthousiaste à l'idée de
partager mes résultats avec lui et de voir qu'il l'était aussi. Ses
évaluations de mes rapports étaient très détaillées et il m'a toujours
aidé à résoudre l'état brumeux de mon esprit induit par de longues
périodes d'étude. Il le faisait en posant des questions cruciales qui
aidaient également l'étude à reprendre son rythme dans les moments
critiques.

Je dois également remercier les utilisateurs du canal Zulip Anand Patel,
André Hernández-Espiet, Eric Wieser, Filippo A. E. Nuccio,
Jireh Loreaux, Joseph Myers, Kevin Buzzard, Kyle Miller, Matt Diamond,
Patrick Massot, Riccardo Brasca, Richard Copley, Ruben Van de Velde,
Sabrina Jewson, Sophie Morel et Yaël Dillies pour leur aide dans le cadre
de la programmation Lean.

Je voudrais également remercier ma famille qui m'a soutenu par ses vœux
et ses prières. En particulier, l'intérêt de mon frère aîné Bayram à
écouter le travail une fois terminé est très précieux pour moi.

Enfin, je voudrais remercier ma compagne, Esra, pour sa patience et pour
avoir toujours été à mes côtés. Sans sa présence et son aide, je n'aurais
jamais commencé à étudier.

\vfill{}
\hfill{} \textit{à Esra}
\vfill{}
\chapter*{Introduction}
Lean est un assistant de preuve. La transcription d'une preuve en
langage humain dans un assistant de preuve est appelée
\textit{formalisation}. Lean dispose d'une grande bibliothèque de
preuves, y compris de nombreuses preuves du niveau de licence, appelée
mathlib4. Dans cette bibliothèque, il y a d'importants théorèmes
manquants, et le théorème de Desargues est l'un d'entre eux.

Les deux aspects principaux de ce projet sont l'apprentissage des
rudiments de la théorie des géométries projectives, et de la
programmation en Lean. Avec ces deux aspects, le but ultime est de
formaliser le théorème de Desargues dans Lean.
\clearpage
\tableofcontents*
\mainmatter
\chapter{Résultats réquis}
\section{Première rencontre}
Pour motiver les géométries projectives, on commence par considérer
les droites passant par l'origine dans le plan. On peut représenter la
plupart de ces lignes par des points sur l'axe $y=1$.
\begin{figure}%[H]
  \centering
  \begin{tikzpicture}
    \draw[-stealth,semithick] (-4,0)--(4,0) node[right] {$x$};
    \draw[-stealth,semithick] (0,-2)--(0,4) node[above] {$y$};
    \draw[name path=y1,semithick] (-3,1)--(3,1) node[right] {$y=1$};
    \draw[name path=line 1,semithick] (1,-1.5)--(-2,3) {};
    \draw[name path=line 2, semithick] (-2,-1.5)--(4,3) {};
    \fill[name intersections={of=y1 and line 1}] (intersection-1) circle (2pt)
    node[below left] {$(-2/3,1)$};
    \fill[name intersections={of=y1 and line 2}] (intersection-1) circle (2pt)
    node[below right] {$(4/3, 1)$};
  \end{tikzpicture}
  \caption{La représentation des droites passant par l'origine dans le
    plan}
  \label{fig:lines-plane}
\end{figure}
La seule droite que l'on n'a pas réussi à représenter est l'axe
$x$. On notera également que l'on peut bien sûr choisir n'importe quel
axe pour la représentation, à l'exception de ceux qui passent par
l'origine. Cette impossibilité dans les cas d'exception est clairement
visible sur la \autoref{fig:lines-plane}. Si l'on choisit un tel axe,
la droite que l'on ne parviendra pas à représenter sera la droite
(passant par l'origine) qui est parallèle à cet axe.

Effectuons la même procédure pour l'espace. On peut représenter la
plupart des droites passant par l'origine par des points sur le plan
$z=1$.
\begin{figure}%[H]
  \centering
  \begin{pspicture}[viewpoint=30 40 30 rtp2xyz] (-5,-2) (5,4)
    \psSolid[object=plan,
    definition=equation,
    args={[0 0 1 0]},
    base=-2 3 -2 2.5]
    \psSolid[object=plan,
    definition=equation,
    args={[0 0 1 -2]},
    base=-2 3 -2 2.5]
    \psSolid[object=point,
    args=0 0 2]
    \psSolid[object=line,
    linestyle=dashed,
    args=0 0 0 -1 0.67 2]
    \psSolid[object=line,
    args=-1 0.67 2 -1.5 1 3]
    \psSolid[object=point,
    args=-1 0.67 2]
    \psSolid[object=line,
    linestyle=dashed,
    args=0 0 0 0.67 -1 2]
    \psSolid[object=line,
    args=0.67 -1 2 1 -1.5 3]
    \psSolid[object=point,
    args=0.67 -1 2]
    \axesIIID[labelsep=10pt] (0.5,0.5,2) (3.5,3.5,3.5)
    \rput(-2,3.05){$(-1/2,1/3,1)$}
    \rput(2.5,3.2){$(1/3,-1/2,1)$}
    \rput(3,1){$z=1$}
  \end{pspicture}
  \caption{La représentation des droites passant par l'origine dans l'espace}
  \label{fig:lines-space}
\end{figure}
Maintenant, les seules droites que nous ne pouvons pas représenter
sont exactement les droites du plan que nous avons représenté
précédemment. La remarque sur le choix de l'axe de représentation
s'étend ici comme tout plan ne passant pas par l'origine peut être
utilisé. De plus, le plan irreprésentable sera celui (qui passe par
l'origine) qui est parallèle au plan de représentation.

Ce processus s'appelle la \textit{projectivisation d'un espace vectoriel}.
Écrivons-le en langage d'algèbre linéaire.
\section{Projectivisation d'un espace vectoriel}
\begin{defn}[{\cite[27]{ff00}}]
  \label{projectivization}
  Soit $V$ un espace vectoriel. Sur
  $V^{\unbutton} \defeq V \setminus \set{0}$, on définit une relation
  binaire comme suit : $x \sim y$ si et seulement si $x, y$ sont
  linéairement dépendants. Comme ceci est une relation
  d'équivalence, l'ensemble quotient
  $\proj(V) \defeq V^{\unbutton} / {\sim}$ est bien défini. $\proj(V)$
  est appelée la \textit{projectivisation de l'espace vectoriel $V$}.
\end{defn}
Pour simplifier le langage, nous aurons également besoin de la
définition de l'union disjointe.
\begin{defn}
  Soit $A$ et $B$ deux ensembles. L'union
  $(A \times \set{1}) \cup (B \times \set{0})$, noté $A \discup B$, est
  appelée \textit{union disjointe} de $A$ et $B$.
\end{defn}
La motivation ci-dessus peut donc être formulée comme suit :
\begin{align*}
  \label{eq:embedding}
  \proj(\R^3) &= \proj(\R^2 \times \R) \\
              &\cong \R^2 \discup \proj(\R^2) \\
              &= \R^2 \discup \proj(\R \times \R) \\
              &\cong \R^2 \discup \R \discup \proj(\R).
\end{align*}
Cela résume ce que l'on fait mathématiquement lorsque l'on fait des
dessins en perspective : On prend un plan ($\R^2$), on choisit un
horizon ($\R$) et un point de fuite ($\proj(\R)$). La proposition
suivante n'est qu'une généralisation de ce processus.
\begin{prop}[{\cite[28]{ff00}}]
  Pour un $K$-espace vectoriel $V$, il existe une bijection naturelle
  \begin{equation*}
    \label{natural-bijection}
    s: \proj(V \times K) \to V \discup \proj(V)
  \end{equation*}
  induite par la fonction
  $t: (V \times K)^{\unbutton} \to V \discup \proj(V)$ définie par
  $t(x,\xi) = \xi^{-1}x$ si $\xi \neq 0$ et $t(x,0) = [x]$ pour
  $x \neq 0$, où $[x]$ désigne le point de $\proj(V)$ représenté par
  $x$.
  % Il existe donc une relation ternaire unique $\overline{\ell}$ sur
  % $V \discup \proj(V)$ pour laquelle $V \discup \proj(V)$ devient
  % une géométrie projective et $s$ un isomorphisme. De plus, on a:
  % \NumTabs{2}
  % \begin{enumerate}[align=left]
  %   \item $\overline{\ell}(x, y, z)$ \tabto{3cm} ssi $x-z$ et $y-z$
  %   sont linéairement dépendants dans $V$,
  %   \item $\overline{\ell}(x, y, [z])$ \tabto{3cm} ssi $x-y = \mu z$
  %   pour un $\mu \in K$
  %   \item $\overline{\ell}(x, [y], [z])$ \tabto{3cm} ssi $[y] = [z]$,
  %   \item $\overline{\ell}([x], [y], [z])$ \tabto{3cm} ssi
  %   $\ell([x], [y], [z])$.
  % \end{enumerate}
\end{prop}

\begin{defn}[{\cite[26]{ff00}}]
  \label{projective-geometry}
  Une \textit{géométrie projective} est un ensemble $G$ accompagné
  d'une relation ternaire $\ell \subseteq G \times G \times G$ telle
  que les axiomes suivants sont satisfaits :
  \begin{itemize}[align=left]
    \item[($\text{L}_1$)] $\ell(a,b,a)$ pour tout $a, b \in G$.
    \item[($\text{L}_2$)] $\ell(a,p,q)$, $\ell(b,p,q)$ et $p \neq q$
          $\implies$ $\ell(a,b,p)$.
    \item[($\text{L}_3$)] $\ell(p,a,b)$ et $\ell(p,c,d)$ $\implies$
          $\ell(q,a,c)$ et $\ell(q,b,d)$ pour un $q \in G$.
  \end{itemize}
  Les éléments de $G$ sont appelés les \textit{points} de la
  géométrie. Et trois points $a, b, c$ sont dits \textit{colinéaires}
  si $\ell(a,b,c)$.
\end{defn}
% Un système équivalent d'axiomes utilisant l'ensemble, par exemple,
% $a \star b$, créé par $\ell$ est omis ici, par souci de
% concision. La définition de morphisme sera donnée à l'aide de ce
% système.

Notons l'exemple le plus important pour une géométrie projective. Lors d'une
\href{https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Missing.20theorems.20list/near/397885401}{discussion}
sur la chaîne de Zulip de Lean, Joseph Myers a conseillé d'énoncer le théorème
sur cet exemple, mais pas sur la définition abstraite d'une géométrie
projective. De plus, il est noté que la version du théorème en géométrie
euclidienne, qui est probablement même connue de nombreux élèves du lycée, peut
être déduite de l'énoncé du théorème sur cet important modèle de géométrie
projective.
\begin{prop}[{\cite[27]{ff00}}]
  \label{example}
  Pour un espace vectoriel $V$, $\proj(V)$ est une géométrie
  projective si pour tout élément $X, Y, Z \in \proj(V)$ on définit :
  $\ell(X,Y,Z)$ si et seulement si $X, Y, Z$ ont des représentants
  $x, y, z$ linéairement dépendants.
\end{prop}
\section{Isomorphismes}
Les isomorphismes seront très utiles tout au long du voyage.
\begin{defn}[{\cite[27]{ff00}}]
  Un \textit{isomorphisme} de géométries projectives est une bijection
  $g: G_1 \to G_2$ satisfaisant $\ell_1(a,b,c)$ si et seulement si
  $\ell_2(ga,gb,gc)$. Si $G_1 = G_2$, alors on dit que $g$ est une
  \textit{collinéation}.
\end{defn}
Toutes les applications linéaires bijectives induisent une
colinéation.
\begin{exm}
  Soit $T: \R^n \to \R^n$ une application linéaire
  bijective. L'application $g: \proj(\R^n) \to \proj(\R^n)$,
  $[x] \mapsto [T(x)]$ est un isomorphisme de géometries projectives.

  L'application $g$ est bien définie: Soit $x, y \in \R^n$ tel que
  $[x] = [y]$, i.e. $x = ky$ pour un $k \in \R$. On a:
  \begin{align*}
    [T(x)] &= [T(ky)] \quad x \ \text{définition} \\
           &= [kT(y)] \quad T \ \text{linéaire} \\
           &= [T(y)] \quad \text{\cref{projectivization}.}
  \end{align*}
  D'où, $g$ est bien définie.

  Montrons que $g$ est injective. Soit $[x], [y] \in \proj(\R^n)$ tel
  que $[T(x)] = [T(y)]$, i.e. $T(x) = kT(y)$ pour un $k \in \R$. Comme
  $T$ est linéaire, $T(x) = T(ky)$. De plus, $x = ky$ car $T$ est
  injective. Par la définition de la classe d'équivalence, on obtient
  $[x] = [y]$. D'où, $g$ est injective. Pour la surjectivité, prenons
  $[x] \in \proj(\R^n)$. Comme $T$ est bijective, $T^{-1}$ existe, et
  $[T^{-1}(x)] \in \proj(\R^n)$. Ainsi
  $g([T^{-1}(x)]) = [T(T^{-1}(x))] = [x]$. D'où, $g$ est
  surjective. On a montré que $g$ est bijective.

  Vérifions la condition d'isomorphisme. Soit
  $[x], [y], [z] \in \proj(\R^n)$. Supposons que
  $\ell([x], [y], [z])$. On a des équivalences:
  \begin{align*}
    &\iff ax + by + cz = 0 \quad \text{\cref{example}} \\
    &\iff T(ax + by + cz) = 0 \quad T \ \text{linéaire, injective} \\
    &\iff aT(x) + bT(y) + cT(z) = 0 \quad T \ \text{linéaire} \\
    &\iff \ell([T(x)], [T(y)], [T(z)]) \quad \text{\cref{example}}
  \end{align*}
\end{exm}
Mais les colinéations sont bien plus que des applications linéaires bijectives.
En d'autres termes, il existe des collinéations qui ne sont pas induites par une
application linéaire.
\begin{exm}
  L'application $g: \proj(\R^2) \to \proj(\R^2)$ définie par
  $[(x_1, x_2)] \mapsto [((x_{1} / x_{2})^3, 1)]$ si $x_{2}$ est non-nul, et
  $[(x_{1}, 0)] \mapsto [(x_{1}, 0)]$ sinon, est une collineation qui n'est pas
  induite par une application linéaire.

  L'application $g$ est bien définie. Soit $x_{1} > 0, x_{2} > 0, x_{1}', x_{2}'$ des
  réels tel que
  $[(x_{1}, x_{2})] = [(x_{1}', x_{2}')]$. Alors, $x_{1}' = kx_{1}$ et
  $x_{2}' = kx_{2}$ pour un $k$ non-nul. On a:
  \begin{align*}
    [((x_{1}' / x_{2}')^{3}, 1)] &= [((kx_{1} / kx_{2})^{3}, 1)] \\
                                 &= [((x_{1} / x_{2})^{3}, 1)]
  \end{align*}
  D'où, $g$ est bien définie.

  Montrons que $g$ est injective. Soit $x_{1}, x_{2}, x_{1}', x_{2}'$ des réels
  tel que
  \[
  [((x_{1} / x_{2})^{3}, 1)] = [((x_{1}' / x_{2}')^{3}, 1)].
  \]
  On va montrer que $[(x_{1}, x_{2})] = [(x_{1}', x_{2}')]$. Par la définition
  de la classe d'équivalence, on a
  \[
  ((x_{1} / x_{2})^{3}, 1) = k ((x_{1}' / x_{2}')^{3}, 1)
  \]
  pour un $k$ non-nul. Alors, $k = 1$ et on a:
  \[
  x_{1} / x_{2} = x_{1}' / x_{2}'.
  \]
  Si $x_{1}$ est nul, alors $x_{1}'$ l'est aussi, et donc on a:
  \begin{align*}
    [(0, x_{2})] &= [(0, \frac{x_{2}'}{x_{2}} x_{2})] \quad \text{ classe
                   d'équivalence définition} \\
                 &= [(0, x_{2}')]
  \end{align*}
  Sinon on a $x_{1} / x_{1}' = x_{2} / x_{2}'$ et donc:
  \begin{align*}
    [(x_{1}, x_{2})] &= [(\frac{x_{1}' x_{2}}{x_{2}'}, \frac{x_{1} x_{2}'}{x_{1}'})] \\
                     &= [(x_{1}', x_{2}')] \quad \text{classe d'équivalence définition}
  \end{align*}
  Enfin, on vérifie la reste de l'image. Soit $x_{3}$ un réel. Il est clair que
  $[((x_{1} / x_{2})^{3}, 1)] \neq [(x_{3}, 0)]$. D'où, $g$ est injective. Pour
  la surjectivité, prenons des réels $x_{1}, x_{2}$. Si $x_{2}$ est nul, on a
  $g([(x_{1}, 0)]) = [(x_{1}, 0)]$. Sinon on a:
  \begin{align*}
    g([(x_{1}^{1/3}, x_{2}^{1/3})]) &= [((x_{1}^{1/3} / x_{2}^{1/3})^{3}, 1)]
                                      \quad \text{$g$ définition} \\
                                    &= [(x_{1} / x_{2}, 1)] \\
                                    &= [(x_{1}, x_{2})]
                                      \quad \text{classe d'équivalence définition}.
  \end{align*}

  $g$ est automatiquement une collinéation car trois vecteurs quelconques sont
  toujours linéairement dépendants dans $\R^2$.

  Montrons maintenant que $g$ n'est pas induite par une application linéaire.
  Supposons par l'absurde que $g$ est induite par l'application linéaire
  $T : \R^{2} \to \R^{2}$. Alors on a $T(1, 0) = (k_{1}, 0)$ et
  $T(0, 1) = (0, k_{2})$ pour $k_{1}, k_{2}$ non-nuls. Soit $x$ un réel.
  D'une part, on a $T(x, 1) = k_{x} (x^{3}, 1)$ pour un $k_{x}$ non-nul, et
  d'autre part, on a $T(x, 1) = x T(1, 0) + T(0, 1)$. Donc, on a:
  \[
  k_{x} (x^{3}, 1) = x (k_{1}, 0) + (0, k_{2})
  \]
  Par conséquent, on obtient l'égalité des polynômes $k_{2}x^{3} = k_{1}x$ qui
  entraîne $k_{1} = k_{2} = 0$. Ceci oblige $T = 0$ qui est absurde.
\end{exm}
\section{Sous-espaces}
Cette partie comprend les structures qui sont importantes pour la
première grande étape du projet. D'abord, on donne une deuxième
axiomatisation.
\begin{prop}
  Soit $G = (G, \ell)$ une géométrie projective. L'opérateur $\star : G
  \times G \to \symcal{P}(G)$ définie par $a \star b \defeq \setcomp{c \in
  G}{\ell (a, b, c)}$ si $a \neq b$ et $a \star a \defeq \set{a}$ ont les
  propriétés suivantes:
  \begin{itemize}[align=left]
    \item[($\text{P}_1$)] $a \star a = \set{a}$ pour tout $a \in G$.
    \item[($\text{P}_2$)] $a \in b \star a$ pour tout $a, b \in G$.
    \item[($\text{P}_3$)] $a \in b \star p$ et $p \in c \star d$ et $a
      \neq c$ implique $(a \star c) \cap (b \star d) \neq \emptyset$.
  \end{itemize}
\end{prop}
\begin{defn}
  Un \textit{sous-espace} d'un géométrie projective $G$ est un
  sous-ensemble $E \subseteq G$ satisfaisant
  \[
  a, b \in E \implies a \star b \subseteq E
  \]
\end{defn}
\begin{defn}
  Un \textit{sous-géométrie projective} d'un géométrie projective $G$ est
  un sous-ensemble $G' \subseteq G$ tel que $G'$ avec la restriction
  $\ell' \defeq \ell \cap (G' \times G' \times G')$ est aussi un
  géométrie projective.
\end{defn}
On s'intéresse au résultat suivant.
\begin{prop}
Tout sous-espace est une sous-géométrie projective.
\end{prop}
On définit également des droites.
\begin{defn}
  Une droite de $G$ est un sous-ensemble de la forme $\delta = a \star
  b$ où $a \neq b \in G$.
\end{defn}
\begin{prop}
  Toute ligne est un sous-espace.
\end{prop}
% Pour arriver à définir les endomorphisms, on note les définitions de
% fonction partielle, de noyau et domaine d'un fonction partielle, de
% sous-espace d'un géométrie projective, de morphisme et d'hyperplan.
% \begin{defn}
%   Une \textit{fonction partielle} de $X$ dans $Y$ est une fonction
%   $f: X \setminus N \to Y$ définie sur le complément d'un
%   sous-ensemble $N \subseteq X$. Si $f$ est une fonction partielle de
%   $X$ dans $Y$, on écrit $f: X \partialto Y$, ou encore $f: X \to Y$
%   si on sait que $N = \emptyset$. L'ensemble $N$ est appelé
%   \textit{noyau} de $f$ et sera désigné par $\kernel f$. L'ensemble
%   $X \setminus N$ est appelé \textit{domaine} de $f$ et sera désigné
%   par $\domain f$.
% \end{defn}
% \begin{defn}
%   Un \textit{sous-espace} d'un géométrie projective $G$ est un
%   sous-ensemble $E \subseteq G$ satisfaisant :
%   \begin{equation*}
%     \label{subspace}
%     a,b \in E \implies a \star b \subseteq E
%   \end{equation*}
% \end{defn}
% \begin{defn}
%   Un \textit{morphisme} d'un géométrie projective $G_1$ dans un
%   géométrie projective $G_2$ est une fonction partielle $g: G_1
%   \partialto G_2$ satisfaisant les axiomes suivant :
%   \begin{itemize}[align=left]
%     \item[($\text{M}_1$)] $\kernel g$ est un sous-espace de $G_1$,
%     \item[($\text{M}_2$)] si $a, b \not\in N$, $c \in N$ et $a \in b
%     \star c$, alors $ga = gb$,
%     \item[($\text{M}_3$)] si $a, b, c \not\in N$ et $a \in b \star c$,
%     alors $ga \in gb \star gc$.
%   \end{itemize}
% \end{defn}
% \begin{defn}
%   Un \textit{hyperplan} d'une géométrie projective $G$ est un
%   sous-espace $H$ de $G$ qui est maximal parmi les sous-espaces
%   stricts de $G$.
% \end{defn}
% Nous définissons enfin les endomorphismes, ainsi que le centre et
% l'axe d'un endomorphisme.
% \begin{defn}
%   Un \textit{endomorphisme} d'un géométrie projective $G$ est un
%   morphisme $\varphi: G \partialto G$. Un \textit{centre} d'un
%   endomorphisme $\varphi: G \partialto G$ est un point $z \in G$ tel
%   que $\varphi x \in x \star z$ pour tout $x \in \domain \varphi$. Un
%   \textit{axe} d'un endomorphisme $\varphi: G \partialto G$ est un
%   hyperplan $H \subseteq G$ tel que $\varphi x = x$ pour tout $x \in H
%   \cap \domain \varphi$.
% \end{defn}
\chapter{Formalisation}
Commençons par transcrire la définition de la géométrie projective
(\cref{projective-geometry}). Il faut d'abord représenter d'une certaine manière
les points, c'est-à-dire les éléments d'une géométrie projective, et la relation
de colinéarité. Les points de la géométrie projective seront abstraits,
c'est-à-dire un \textit{type}. La relation de colinéarité peut être représentée
par une fonction qui prend trois points et renvoie vrai ou faux ; après tout,
lorsque l'on dit qu'une relation $\ell$ est valable, ce que l'on fait, c'est
prendre trois points et se demander s'ils sont colinéaires ou non.
\begin{leancode}
class HasCollinear (P : Type) where
ell : P → P → P → Prop

export HasCollinear (ell)

variable {Point : Type} [HasCollinear Point]
\end{leancode}
Ici, la flèche entre les types \texttt{P} peut être considérée comme
la flèche entre le domaine et le codomaine dans les définitions de
fonctions dans le langage habituel des mathématiques, c'est-à-dire le
symbole \say{$\to$}.

Comme le point reste abstrait, il a fallu dire à Lean que l'existence
d'une interprétation de la colinéarité est assurée, c'est-à-dire que
la colinéarité des points est quelque chose que l'on peut décider.
Dans le code, cela est satisfait par la dernière ligne :
\texttt{Point} est un type dont la colinéarité existe.

Maintenant, on peut énoncer les axiomes $\text{L}_1$, $\text{L}_2$ et
$\text{L}_3$ dans la \cref{projective-geometry}.
\begin{leancode}
axiom l1 (a b : Point) : ell a b a
axiom l2 (a b p q : Point) : ell a p q → ell b p q → p ≠ q →
                             ell a b p
axiom l3 (a b c d p: Point) : ell p a b → ell p c d →
                              ∃ q : Point,
                              ell q a c ∧ ell q b d
\end{leancode}
Il y a quelques points à noter ici. Tout d'abord, les flèches
utilisées ici sont différentes de celles que nous avons utilisées
ci-dessus, même si elles sont représentées par le même caractère
typographique : Il s'agit de flèches d'implication, pour lesquelles
nous utilisons normalement le symbole
\say{$\Longrightarrow$}. Deuxièmement, les conditions des axiomes qui
contiennent des conjonctions logiques sont converties en implications
sérielles. Expliquons cette équivalence logique. Supposons qu'on a une
condition de la forme $(p \land q) \implies r$. On a des équivalences
suivantes:
\begin{align*}
  &\iff \neg(p \land q) \lor r \\
  &\iff (\neg p \lor \neg q) \lor r \\
  &\iff \neg p \lor (\neg q \lor r) \\
  &\iff p \implies (\neg q \lor r) \\
  &\iff p \implies (q \implies r)
\end{align*}
Grâce à ces axiomes, nous pouvons prouver la proposition suivante.
\begin{prop}
  Toute relation ternaire $\ell$ qui satisfait les deux axiomes
  $\text{L}_1$ et $\text{L}_2$ est symétrique.
\end{prop}
Dans la preuve, on va dériver la colinéarité de toutes les
permutations possibles de trois points $a, b, c$ à partir de
$\ell(a, b, c)$. Ici, on ne donnera que $\ell(a, c, b)$ et les cinq
autres versions seront omises.
\begin{leancode}
theorem acb
  (a b c : Point)
  (abc_col: ell a b c) :
    ell a c b := by
  intro abc_col -- Supposons que $\ell(a,b,c)$.
  obtain rfl | bc_neq := eq_or_ne b c -- Si $b = c$,
  exact abc_col -- le résultat est trivial,
  apply l2 a c b c -- sinon on applique $\text{L}_2$;
  exact abc_col -- première condition de $\text{L}_2$
  apply l1 c b -- deuxième condition de $\text{L}_2$
  exact bc_neq -- troisième condition de $\text{L}_2$.
\end{leancode}
Ce code est la transcription exacte de la phrase \say{Si $b = c$, le résultat
  est trivial, et sinon on applique $\text{L}_2$ à $\ell(a,b,c)$ et
  $\ell(c,b,c)$}.
\section{Regrouper le point et les axiomes}
Cette proposition la plus simple peut être considérée comme un premier théorème
prouvé avec cette configuration. Des théorèmes plus ambitieux peuvent également
être prouvés, mais décrire une géométrie projective en déclarant son point et
axiomes les uns après les autres n'est pas la manière la plus élégante. Pour
l'instant, ils n'ont qu'une relation sérielle dans le fichier. Ce qui est plus
utile, c'est une structure qui contiendrait toutes les informations nécessaires
à une géométrie projective. La structure suivante répond à ce besoin :
\begin{leancode}
class ProjectiveGeometry
  (point : Type u) where
  ell : point → point → point → Prop
  l1  : ∀ a b, ell a b a
  l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d →
                     ∃ q : point, ell q a c ∧ ell q b d
\end{leancode}
De cette manière, on a \textit{regroupé} la relation de colinéarité et
les axiomes (\say{bundling}), et le point est resté \textit{dégroupé}
(\say{unbundled}) parce qu'il s'agit d'un paramètre et que l'on veut que
différents types de points correspondent à différentes géométries
projectives. Pour mieux expliquer le contraste, on ne veut pas que des
relations de colinéarité différentes correspondent à des géométries
projectives différentes ; on pense à une relation de colinéarité
canonique pour obtenir une géométrie projective. Ceci est expliqué en
détail
\href{https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Creating.20a.20higher.20level.20object/near/423444220}{ici}.
\section{Instances}
Il est maintenant possible de déclarer que la projectivisation d'un espace
vectoriel est une géométrie projective.
\begin{leancode}
instance : ProjectiveGeometry (ℙ K V) :=
  ⟨
  fun X Y Z => ¬ Independent ![X, Y, Z],
  sorry,
  sorry,
  sorry
  ⟩
\end{leancode}
Expliquons comment cela fonctionne : Tout d'abord, une relation de colinéarité
sera fournie. Celle-ci est déjà établie mathématiquement dans la \cref{example}.
La fonction \texttt{Independent} provient de mathlib4. Elle prend trois points
de la projectivisation et affirme que leurs représentants sont linéairement
dépendants. Sur le plan technique, il prend une famille de points de
projectivisation. Une famille est une fonction d'indices dans des points.
Heureusement, mathlib4 dispose d'une syntaxe pour convertir une liste en une telle
fonction : \say{\texttt{!}}. Si elle n'existait pas, on devrait l'écrire
manuellement :
\begin{leancode}
def indexer_generator
  (X Y Z : ℙ K V) :
    Fin 3 → ℙ K V :=
  fun i : Fin 3 => match i with
  | 0 => X
  | 1 => Y
  | 2 => Z
\end{leancode}

Ensuite, les axiomes seront vérifiés. Lean remplacera la relation de colinéarité
dans les axiomes pour nous. Les \say{sorry} servent de substitut à des preuves
qui n'ont pas encore été écrites.

Ainsi, nous pouvons continuer à étudier le côté purement synthétique et nos
résultats s'appliqueront automatiquement à la projectivisation d'un espace
vectoriel : Le côté concret. Pour les choses qui sont spécifiques aux
projectivisations, nous pouvons bien sûr passer du côté concret et continuer à
développer des propriétés pour elles.
\section{Les yeux fermés}
Une chose que j'ai souvent constatée tout au long de mon parcours, c'est
que le livre est extrêmement prudent dans ce qu'il fait et ce qu'il dit.
L'une de mes dernières expériences a été de réaliser que la fonction de
colinéarité devrait en fait être dégroupé. Je m'en suis rendu compte une
fois que j'ai essayé de montrer qu'un ensemble ayant deux fonctions de
colinéarité différentes peut en fait être deux géométries projectives
différentes, mais la fonction de colinéarité étant groupée, il était
impossible de l'énoncer en premier lieu. En fait, nous devrions énoncer
la classe de géométrie projective comme suit :
\begin{leancode}
class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  l1  : ∀ a b , ell a b a
  l2  : ∀ a b p q , ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d →
        ∃ q, ell q a c ∧ ell q b d
\end{leancode}
Cela correspond en fait à la définition donnée dans le livre : Une
géométrie projective est un ensemble $G$ avec une relation de colinéarité
$\ell$\ldots{} J'ai tiré deux leçons de cette expérience : La première est
que lors de la formalisation d'un livre, il faut essayer de comprendre
les intentions de l'auteur, en particulier lorsqu'une définition de base
est donnée. La seconde est que, si le livre est suffisamment prudent
(formel, rigoureux\ldots), il peut être possible de formaliser les yeux
fermés. Par les yeux fermés, je veux dire formaliser comme un robot, dans
un état pas particulièrement attentif.

Cela a été possible de manière très surprenante dans de nombreux cas. Je
ne faisais qu'appliquer syntaxiquement les phrases des preuves les unes
après les autres. Bien sûr, j'ai souvent pensé aux mécanismes (tactiques,
structures ou autres caractéristiques du langage Lean) nécessaires à
l'élaboration de la preuve donnée dans le livre, mais une fois cela fait,
le travail consistait simplement à exécuter la preuve avec soin. C'est,
encore une fois de manière surprenante, possible parce qu'il y a un
vérificateur de preuves qui crie constamment la prochaine chose à
montrer. Sans lui, il n'est pas possible d'avancer dans la preuve sans
réfléchir.
\section{Dépendances}
J'ai été enthousiasmé de voir que les épreuves données dans le livre
fonctionnaient bien. Cela passe par l'efficacité des preuves, la mention
claire et explicite des propriétés, remarques, propositions ou théorèmes
précédents montrés. Le livre a un sens de l'ordre très précis ; en tant
qu'étudiant de licence, j'étais un peu timide à l'approche du
livre, mais avec le temps et sa précision, je me suis continuellement
familiarisé avec le livre.

Maintenant que j'ai parlé de la nature du livre, je devrais peut-être
continuer à l'expliquer en détail. Le livre est un traité de géométrie
projective avec morphismes. Il s'agit d'une géométrie projective
axiomatique, et non d'une géométrie projective analytique. Et les
morphismes sont des fonctions partielles, et non des fonctions à
proprement parler. Le livre explique que c'est peut-être la raison pour
laquelle il n'existe pas de traitement systématique de la géométrie
projective avec morphismes. Le livre ajoute ensuite : \say{Nous avons
  l'intention de combler cette lacune. C'est en ce sens que la présente
  monographie peut être qualifiée de moderne}.

Il semble que l'ambition d'utiliser l'algèbre se soit étendue à d'autres
parties du livre, car celui-ci utilise également la théorie des treillis
et la théorie des catégories pour diverses parties de la géométrie
projective. Pour le meilleur ou pour le pire, j'ai maintenant une
certaine compréhension de la façon dont différentes abstractions peuvent
être utilisées et incorporées lors de la construction d'une théorie. En
particulier dans la théorie des treillis, j'ai apprécié l'utilisation de
l'opérateur $\vee$ dans la définition de l'hyperplan.

Mais cette généralité a été un obstacle pendant la plus grande partie du
voyage. J'essayais constamment de réduire ces notations et ces
définitions parfois riches en formes pures. Par formes pures, j'entends
les formes n'impliquant que les axiomes de la géométrie projective et les
définitions que j'avais données jusqu'alors. Cette réduction était très
difficile, d'une part parce que je devais apprendre une nouvelle théorie
à partir de zéro et me familiariser avec ses notations, et d'autre part
parce que je n'avais pas le temps de me familiariser avec la géométrie
projective. Donnons la définition d'un hyperplan.
\begin{defn}[{\cite[38]{ff00}}]
  Un \textit{hyperplan} d'une géométrie projective $G$ est un
  sous-espace $H$ de $G$ qui est maximal parmi les sous-espaces
  stricts de $G$.
\end{defn}
Immédiatement après la définition, nous avons la proposition énonçant les
conditions équivalentes pour être un hyperplan.
\begin{prop}
  Pour un sous-espace $H$ d'une géométrie projective $G$, les conditions
  suivantes sont équivalentes :
  \begin{itemize}
    \item $H$ est un hyperplan,
    \item $H$ est un sous-espace strict et pour tout point $a \in H$ on a
      $a \vee H = G$,
    \item il existe un point $a \not \in H$ tel que $a \vee H = G$,
    \item $H \neq G$ et pour tout point $a \neq b$ on a $(a \star b) \cap
      H \neq \emptyset$.
  \end{itemize}
\end{prop}
Ici, nous pouvons voir à la fois la forme pure, la forme théorique du
treillis et le mélange des deux. L'objectif de cette proposition est en
fait de les coller, de sorte que chacune d'entre elles puisse être
utilisée librement par la suite. Mais du côté de la formalisation, c'est
difficile. Il y a deux options pour les chemins à prendre. La première
consiste à formaliser également les définitions et théorèmes de la
théorie des treillis nécessaires, ou à les utiliser à partir de mathlib4
s'ils sont déjà formalisés, ce qui n'est pas toujours une opération
parfaitement aisée. L'autre consiste à traduire à la main toutes les
définitions et théorèmes de la théorie des treillis en formes pures et à
les utiliser. Ici, nous avons heureusement une forme pure, mais lorsque
le livre utilisera librement les théorèmes de treillis plus tard, nous
serons coincés. Il s'agit donc d'un aspect dont il faut être conscient
dans le cadre de la formalisation. Je pense pouvoir dire en toute
confiance que cela a été la partie la plus sophistiquée, la plus longue
et la plus fastidieuse de l'aventure.
\section{Progression et régression}
Maintenant que j'ai expliqué certains thèmes de la formalisation, il est
temps de mentionner quelques phénomènes de haut niveau. Lorsque j'ai
commencé à étudier, ma stratégie consistait à acquérir une compréhension
générale de la géométrie projective et de la preuve du théorème de
Desargues, puis à trouver des solutions en cours de route. Cela n'a pas
mal marché, mais il convient de noter que ce n'était pas du tout bien
défini. Une compréhension générale est bien sûr nécessaire, et trouver
des solutions en cours de route peut sembler pragmatique, mais lorsque je
me suis finalement assis et que j'ai essayé de mettre en œuvre, j'ai
immédiatement vu que le début est facile, mais que les conséquences
seront dures. En effet, j'ai changé mes formulations un nombre
incalculable de fois. Plus tard, j'ai réalisé que ce remaniement constant
était en fait une partie importante du voyage.

Ensuite, lorsque j'arrive à un point stable, où je suis satisfait de mes
formulations et où je n'obtiens aucune erreur du vérificateur de type, je
me vois souvent un peu perdu, comme si je devais me demander quelle est
la prochaine chose à énoncer ou à prouver, à nouveau. C'est la
malédiction de l'approche progressive, et cela m'a incité à attaquer le
problème de manière régressive.

L'approche régressive consiste à partir du dernier théorème à prouver et
à déterminer ce qui est nécessaire pour le prouver en termes de
définitions et de théorèmes, jusqu'à ce que toutes les lacunes soient
comblées. Cette approche présente ses propres difficultés. Les
dépendances augmentent de façon exponentielle et je me perds à les
suivre. Pour faciliter le processus, j'ai décidé, à un moment donné,
d'utiliser \texttt{Emacs/org-roam}.

Org-roam permet de travailler avec des noeuds. Dans chaque noeud, je
conserve une définition ou un théorème. L'intérêt est de pouvoir les
relier entre eux. J'obtiens ainsi une toile de définitions et de
théorèmes. Ce qui est encore plus intéressant, c'est de pouvoir
visualiser ce réseau, de manière totalement interactive. Cette méthode de
travail a considérablement développé ma compréhension de la pratique des
mathématiques. Je pense que tout mathématicien devrait au moins utiliser
une fois cette méthode de construction d'un arbre de dépendance.

Je n'ai pas pu terminer complètement l'arbre de dépendance, mais je pense
en avoir réalisé une assez grande partie. Analysons-le.
\begin{sidewaysfigure}
  \centering
  \tiny
  \includesvg[width=\textwidth]{figures/dependency-tree.svg}
  \caption{L'arbre de dépendance de la preuve du théorème de Desargues.}
  \label{fig:dep-tree}
\end{sidewaysfigure}
Tout d'abord, notez qu'il s'agit d'une génération automatique de
graphiques, c'est un fichier \texttt{svg} de haute qualité. Le théorème
final se trouve en haut de la figure. Il s'agit de la projectivisation
des espaces vectoriels, c'est-à-dire le théorème de Desargues habituel
pour les élèves du secondaire. Immédiatement après, nous avons la forme
générale du théorème.

La forme générale dépend de deux définitions majeures : La
\textbf{géométrie arguésienne} et le \textbf{plongement de sous-espace}.
Ceci est logique et probablement visible par la plupart des lecteurs.
Mais en y regardant de plus près, on s'aperçoit que les définitions de
l'\textbf{hyperplan} et des \textbf{morphismes} sont respectivement
reliées par quatre et trois flèches. En d'autres termes, ils ont le plus
grand nombre de liens de retour parmi les nœuds : Ce sont des nœuds
centraux. Nous disons que de telles choses sont des concepts centraux.
Mais dans le graphique, nous disposons d'une mesure quantifiée de
l'importance d'un concept.

Ce fut très instructif, et je pense pouvoir dire que ce fut la partie la
plus utile du voyage de formalisation.

Pour conclure mes propos sur les dépendances, j'ajouterai une petite
découverte que j'ai faite lorsque je transcrivais le ($\text{P}_9$).
Jusqu'à ce moment-là, toutes les transcriptions étaient presque mot à
mot, phrase à phrase aux details de Lean près. Dans ($\text{P}_9$), à la
dernière phrase, je lis \say{\ldots et par ($\text{P}_4$) on conclut
que\ldots}, mais il faut en fait appliquer ($\text{P}_4$) deux fois.
Dans la preuve de ($\text{P}_8$), je lis \say{\ldots en appliquant deux
fois ($\text{P}_7$).}, donc quand il faut appliquer un théorème deux
fois, c'est indiqué dans le livre. Donc, soit on l'a oublié, soit il
s'agit d'une omission incohérente.
\section{Décidabilité}
Lors de la définition de l'opérateur $\star$, il faut supposer que
l'égalité de deux éléments de $G$ est décidable.
\begin{leancode}
variable [DecidableEq G]
\end{leancode}
Voici la définition de l'opérateur $\star$.
\begin{leancode}
def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}
\end{leancode}
Lorsque nous omettons l'égalité décidable de $G$, nous obtenons l'erreur
:
\begin{leancode}
-- failed to synthesize instance
--   Decidable (a = b)
\end{leancode}
\section{Simplification}
Comme la plus grande partie du travail consiste à réécrire l'expression
de l'objectif, il est utile de disposer d'une automatisation pour cela.
Lean a cette syntaxe où vous mettez la balise
%\texttt{@[simp]}
\mintinline{lean}{@[simp]}
juste avant une définition ou un théorème qui énonce une égalité, la
tactique \texttt{simp} applique automatiquement ces définitions et
théorèmes balisés à l'objectif. La définition de l'opérateur $\star$ est
assez appropriée pour cela. Voici la version balisée de la définition :
\begin{leancode}
@[simp]
def star
  [ProjectiveGeometry G ell]
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}
\end{leancode}
\chapter{Conclusion}
Je me souviens avoir été averti par Yaël Dillies que la formalisation de
la géométrie est étonnamment trompeuse. Je comprends maintenant que c'est
peut-être le cas parce que la preuve de ($\text{P}_5$) fait 53 lignes et
celle de ($\text{P}_9$) 77 lignes de code. Leurs versions informelles
sont toutes deux de 5 lignes. Dans les deux, il y a de nombreux cas où je
dois considérer à plusieurs reprises les cas où deux points sont
distincts ou non. Et dans la preuve informelle, ces cas sont omis, pour
de bon. Je pense que pour continuer ce projet, il faut absolument avoir
une automatisation qui gère ces analyses de cas creux. Ce besoin
d'automatisation apparaît également lorsque je prouve la symétrie de la
relation de colinéarité. Les preuves ne sont que des applications de la
permutation. Il est possible d'appliquer correctement les permutations ou
d'effectuer une recherche par force brute. Dans le cas où nous avons $3!
- 1$, il ne s'agit pas vraiment d'une recherche longue.

En dehors de ce goulot d'étranglement technique, les bases sont
formalisées. Il est démontré que les droites sont des sous-espaces, et
que les sous-espaces sont des sous-géométries projectives. C'est l'étape
à laquelle se trouve le projet, à la fin de l'étude.

Pour poursuivre la formalisation, il faut absolument compléter le graphe
de dépendance. Ensuite, tous les théorèmes requis devraient être énoncés
et assumés. L'objectif est que le théorème de Desargues soit énoncé, mais
non prouvé. Les lacunes peuvent être comblées à l'aide du livre, je ne
pense pas que ce soit si difficile à ce stade.
\backmatter
\nocite{*}
\printbibliography[title=Références]
\end{document}