Introduction aux mathématiques formalisées

Les mathématiques se préoccupent de nombreux types d'objets : des nombres, des figures géométriques, des fonctions, des opérations etc... Initialement, la plupart de ces objets proviennent de notre expérience du monde qui nous entoure, mais tous ont fait l'objet d'un processus d'idéalisation et de tri de l'information. Ainsi le nombre 3 est l'objet mathématique abstrait extrait d'une multitude de collections de trois choses, c'est le point commun entre une collection de trois élèves, trois chaises ou trois idées. Cette extraction d'un concept mathématique débute donc dès la maternelle. Plus tard on rencontre la notion de figure géométrique, la notion de point n'ayant ni largeur ni longueur ni épaisseur, la notion de rectangle dont les côtés n'ont aucune épaisseur et dont les angles mesurent exactement un quart de tour.

Le premier intérêt de ce processus est la simplification qui en résulte : le nombre trois oublie toute la complexité des objets de la collection dont on parle, un rectangle est bien plus simple qu'un livre de forme approximativement rectangulaire. Cette simplification permet de se concentrer sur les aspects d'un objet qui sont pertinents pour la discussion en cours. Le processus d'abstraction permet aussi d'affirmer en une seule phrase quelque chose à propos d'un ensemble d'objets. Ainsi l'affirmation « les diagonales d'un rectangle se coupent en leurs milieux » porte sur tous les rectangles. On en déduit un propriété (approximative) de tous les objets du monde réel qui sont (approximativement) des rectangles. Cette possibilité repose sur un autre bénéfice du processus d'abstraction : au contraire des autres sciences et de la vie quotidienne, les mathématiques profitent de l'existence d'affirmations qui sont vraies ou fausses, sans aucune négociation ni nuance. Ces affirmations sont appelées énoncés ou propositions mathématiques. Par exemple « 2 est pair » et « 1 + 1 = 3 » sont des énoncés. Le premier est vrai, tandis que le second est faux.

L'abstraction permet et nécessite le raisonnement logique rigoureux. Elle le permet car les objets manipulés sont suffisamment idéalisés pour que les énoncés deviennent vrais de façon définitive et non ambiguë. Elle le nécessite car elle éloigne de l'intuition immédiate. On peut même dire que ce qui distingue essentiellement les énoncés vrais est qu'on peut les démontrer. Une démonstration est un enchaînement de raisonnements logiques élémentaires permettant de combiner des énoncés vrais à l'aide d'un petit nombre de règles pour obtenir de nouveaux énoncés vrais. L'objectif de ce cours est d'expliciter ces règles et de pratiquer la démonstration et la rédaction de démonstration.

Bien sûr la combinaison d'énoncé vrais au moyen de règles logiques ne peut démarrer qu'en s'appuyant sur un certain nombre d'énoncés fondamentaux non démontrés, qu'on appelle des axiomes. La description d'axiomes n'est pas un objectif de ce cours, qui ne remontera jamais aussi loin dans la chaîne des raisonnements mathématiques. En réalité la manipulation des axiomes n'est l'activité quotidienne que d'une minorité infime de mathématiciens, sans parler des utilisateurs de mathématiques qui ne sont pas mathématiciens et peuvent entièrement ignorer ces axiomes durant toute leur vie. Ainsi c'est bien le raisonnement logique déduisant des énoncés nouveaux à partir d'énoncés supposés vrais qui joue le premier rôle plutôt que les axiomes. Cette observation permet d'évacuer au passage l'épineuse question philosophique de la définition du mot « vrai » pour la remplacer par la question bien plus simple de la validité du raisonnement qui, répétons-le, repose sur un petit nombre de règles très bien définies.

À ce stade il est important de ne pas perdre de vue l'objectif initial de manipulation et de compréhension des objets mathématiques. Le mécanisme du raisonnement logique est indispensable à la pratique mathématique, mais ce n'en est pas l'objet (sauf dans la branche spécialisée de la théorie de la démonstration). De même que la musique ne se réduit ni au solfège ni à la lutherie, et de même que la littérature ne se réduit pas à la grammaire ou à la syntaxe, les mathématiques ne se réduisent pas à la logique. Cependant, de même qu'il est impossible de faire de la musique sans un minimum de le solfège ou d'écrire sans grammaire, on ne peut faire de mathématique sans logique ni démonstration. Et il ne suffit pas d'avoir rencontré les règles de logique, il est nécessaire d'avoir des automatismes, des réflexes.

De même qu'on ne peut pas faire de sport en réfléchissant à la succession des muscles à contracter, on ne peut pas faire de mathématiques sans un certain nombres de réflexes de manipulation formelle des énoncés et objets, complètement indépendamment de leur signification. L'activité mathématique est faite d'oscillations incessantes entre l'intuition et la rigueur logique, entre la créativité et la manipulation formelle de symboles.

Ce cours utilise l'assistant de démonstration Lean, un logiciel dédié à la vérification de démonstrations développé principalement par Leonardo de Moura au sein de Microsoft Research. L'objectif le plus visible de cette utilisation est de vérifier l'application stricte des règle logiques. Mais son objectif principal est de fournir en temps réel le contexte de chaque étape de raisonnement, c'est à dire la collection des objets mathématiques introduits par l'énoncé à démontrer et par les étapes antérieures.

Dans Lean, le mot énoncé est noté Prop. Pour exprimer que « 1 + 1 = 3 » est un énoncé, on écrit 1 + 1 = 3 : Prop. Pour tout énoncé $P$, une hypothèse $h$ affirmant que $P$ est vrai s'écrit h : P. On peut aussi lire cela comme « $h$ est une démonstration de $P$ ».

Le cours alternera entre les exercices de logique abstraite et les démonstrations reprises du cours d'analyse du premier semestre. Voici un exemple de démonstration typique de ce dernier cas. Bien sûr toutes les commandes seront discutées dans la suite. L'objectif immédiat est simplement d'avoir une idée de comment le logiciel se présente.

Dans cet exemple, comme dans tous les autres, on affiche en alternance le texte mathématique usuel et les commandes Lean correspondantes. Chaque ligne de code Lean commence et finit par une zone cliquable grise qui déclenche l'affichage du contexte local, listant objets mathématiques et hypothèses, et de l'énoncé à démontrer, précédé du symbole . Dans une démonstration sans embranchement logique, le contexte au début d'une ligne est évidemment le même qu'à la fin de la ligne précédente. Bien sûr ce contexte n'est pas affiché à l'impression sur papier.

Définition
Soit $f$ une fonction de $ℝ$ dans $ℝ$, et soit $x_0$ et $y_0$ deux nombres réels. On dit que $f$ tend vers $y_0$ en $x_0$ si $ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x_0| ≤ δ ⇒ |f(x) - y_0| ≤ ε$
def limite_fonction (f :   ) (x₀ y₀ : ) : Prop :=
 ε > 0,  δ > 0,  x, |x - x₀|  δ  |f x - y₀|  ε
Définition
Une $u$ de nombres réels tend vers un réel $x_0$ si $∀ ε > 0, ∃ N, ∀ n ≥ N, |u_n - l| ≤ ε$.
def limite_suite (u :   ) (l : ) : Prop :=
 ε > 0,  N,  n  N, |u n - l|  ε
Exemple

Si une suite $u$ tend vers $x_0$ et si une fonction $f$ tend vers $y_0$ en $x_0$ alors la suite $f ∘ u$ (de terme général $f(u_n)$) tend vers $y_0$.

example (f u x₀ y₀) (hu : limite_suite u x₀)
  (hf : limite_fonction f x₀ y₀) : limite_suite (f  u) y₀ :=
Démonstration
Soit $ε$ un réel strictement positif
  intros ε ,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
hf : limite_fonction f x₀ y₀
 limite_suite (f  u) y₀
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
hf : limite_fonction f x₀ y₀,
ε : ,
 : ε > 0
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
Notre but est de montrer qu'il existe un entier $N$ tel que,pour tout entier $n$ supérieur à $N$, $|f(u_n) - y_0|$ est inférieurà $ε$.Par hypothèse de limite sur $f$, appliquée à cet $ε$ strictement positif,il existe un réel $δ$ strictement positif tel que :Pour tout $x$ réel, si $|x - x_0| ≤ δ$ alors $|f(x) - y_0| ≤ ε$ (1).
  specialize hf ε ,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
hf : limite_fonction f x₀ y₀,
ε : ,
 : ε > 0
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
hf :  (δ : ) (H : δ > 0),  (x : ), |x - x₀|  δ  |f x - y₀|  ε
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
Fixons un tel réel $δ$.
  rcases hf with δ, , Hf⟩,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
hf :  (δ : ) (H : δ > 0),  (x : ), |x - x₀|  δ  |f x - y₀|  ε
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
De même l'hypothèse de limite sur $u$, appliquée au réel $δ$ strictementpositif que nous venons de fixer, permet de fixer un entier $N$ telque, pour tout entier $n$, si $n ≥ N$ alors $|u_n - x_0| ≤ δ$ (2).
  rcases hu δ  with N, Hu⟩,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
Montrons que cet entier convient.
  use N,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ
  (N : ),  (n : ), n  N  |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ
  (n : ), n  N  |(f  u) n - y₀|  ε
Soit $n$ un entier supérieur à $N$.
  intros n hn,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ
  (n : ), n  N  |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ,
n : ,
hn : n  N
 |(f  u) n - y₀|  ε
Montrons que $|f(u_n) - y_0| ≤ ε$.Vu la propriété (1), appliquée à $u_n$, il suffit de montrer que$|u_n - x_0| ≤ δ$.
  apply Hf,
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ,
n : ,
hn : n  N
 |(f  u) n - y₀|  ε
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ,
n : ,
hn : n  N
 |u n - x₀|  δ
Cela découle immédiatement de la propriété (2) et de notre hypothèse sur $n$
  exact Hu n hn
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ,
n : ,
hn : n  N
 |u n - x₀|  δ
f :   ,
u :   ,
x₀ y₀ : ,
hu : limite_suite u x₀,
ε : ,
 : ε > 0,
δ : ,
 : δ > 0,
Hf :  (x : ), |x - x₀|  δ  |f x - y₀|  ε,
N : ,
Hu :  (n : ), n  N  |u n - x₀|  δ,
n : ,
hn : n  N
 |u n - x₀|  δ
QED.

Le logiciel Lean est installé en salle informatique du bâtiment 307, mais on peut trouver des instructions d'installation sur cette page. On peut aussi utiliser Lean en ligne sur CoCalc, même si le résultat est un peu capricieux. Les feuilles de TP et l'énoncé sur DM sont dans cette archive. Chaque chapitre de ces notes de cours contient aussi des liens vers des versions des TD s'exécutant directement dans le navigateur web, à condition d'être patient. Les commandes Lean utilisées dans ce cours seront introduites au fur et à mesure mais on peut aussi consulter l'aide-mémoire.

Plan du cours