Lean 6 - Mathlib4 : La Bibliotheque Mathematique

Navigation : ← Lean-05-Tactics-Lean | Index | Lean-07-LLM-Integration-Lean-Python →

Introduction

Ce notebook explore Mathlib4, la bibliotheque mathematique communautaire pour Lean 4. Avec plusieurs millions de lignes de code formalise (Mathlib/ + Archive + scripts), des milliers de modules .lean, et plus de 300 contributeurs actifs (GitHub API, 5+ commits), Mathlib est devenue la reference mondiale pour les mathematiques formelles.

Pourquoi Mathlib est revolutionnaire

Vérification formelle : Chaque théorème est prouvé par machine, garantissant l’absence d’erreurs
Reutilisabilite : Les preuves existantes servent de base pour de nouvelles decouvertes
Collaboration : Des mathematiciens du monde entier contribuent
IA-ready : Infrastructure de vérification formelle (Lean 4 + Mathlib servent de substrate ; AlphaProof s’appuie sur Lean pour la preuve formelle et n’utilise pas Mathlib comme jeu de données d’entrainement direct — vérifié firsthand via DeepMind blog + arXiv:2404.12534 (LeanCopilot/NeuS 2025))

Objectifs pedagogiques

Comprendre la structure et l’organisation de Mathlib4
Installer et configurer Mathlib dans un projet Lean
Maitriser les tactiques puissantes : ring, linarith, omega, norm_num
Naviguer dans la documentation et chercher des théorèmes
Utiliser Mathlib pour des preuves non triviales

Prerequis

Notebooks Lean-1 a Lean-5 completes
Connexion internet pour télécharger Mathlib

Duree estimee : 45-50 minutes

Contexte : L’Ecosysteme Mathlib

Historique

Annee	Événement
2017	Creation de Mathlib pour Lean 3
2023	Migration complète vers Lean 4 (Mathlib4)
2024	Utilisation par AlphaProof (IMO medaille argent)
2025	Terry Tao formalise des résultats en théorie analytique
2026	Lean4Lean presente a POPL (bootstrap de Lean en Lean)

État actuel (Janvier 2026)

Version : v4.32.1 (juillet 2026, derniere stable ; v4.33.0-rc1 en pre-release)
Taille : plusieurs millions de lignes (Mathlib/ + Archive + scripts), des milliers de fichiers .lean (Archive + Lean 3 archive inclus)
Contributeurs : 100+ réguliers, 500+ occasionnels
Utilisateurs notables : Terry Tao (Fields Medal), Kevin Buzzard (Imperial)
Repository : https://github.com/leanprover-community/mathlib4
Documentation : https://leanprover-community.github.io/mathlib4_docs/

1. Installation et Configuration

1.1 Créer un projet avec Mathlib

Mathlib s’installe via Lake, le gestionnaire de paquets Lean 4.

1.1 Créer un projet avec Mathlib (Terminal)

Mathlib s’installe via Lake, le gestionnaire de paquets Lean 4. Voici les commandes a exécuter dans un terminal :

# Créer un nouveau projet avec Mathlib
lake new mon_projet math
cd mon_projet

# Télécharger les dependances
lake update

# Télécharger le cache compile (IMPORTANT - economise des heures!)
lake exe cache get

Structure du projet resultant :

mon_projet/
├── lakefile.lean      # Configuration Lake
├── lean-toolchain     # Version de Lean
├── MonProjet.lean     # Point d'entrée
└── lake-manifest.json # Versions des dependances

Note : Le téléchargement initial de Mathlib4 peut prendre 10-20 minutes et ~1 Go d’espace disque. Le cache precompile (lake exe cache get) evite de tout recompiler.

1.2 lakefile.lean type pour Mathlib

Le fichier lakefile.lean configure les dependances du projet. Pour Mathlib, il specifie la version et permet de télécharger le cache precompile avec lake exe cache get.

-- Exemple de lakefile.lean pour un projet Mathlib
/-
import Lake
open Lake DSL

package "mon_projet" where
  version := v!"0.1.0"

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

@[default_target]
lean_lib «MonProjet» where
  -- Configuration additionnelle si necessaire
-/

-- Exemple de lakefile.lean pour un projet Mathlib

/-

import Lake

open Lake DSL

package "mon_projet" where

  version := v!"0.1.0"

require mathlib from git

  "https://github.com/leanprover-community/mathlib4"

@[default_target]

lean_lib «MonProjet» where

  -- Configuration additionnelle si necessaire

-/

--% env 0

Raw input

{"cmd": "-- Exemple de lakefile.lean pour un projet Mathlib\n/-\nimport Lake\nopen Lake DSL\n\npackage \"mon_projet\" where\n  version := v!\"0.1.0\"\n\nrequire mathlib from git\n  \"https://github.com/leanprover-community/mathlib4\"\n\n@[default_target]\nlean_lib \u00abMonProjet\u00bb where\n  -- Configuration additionnelle si necessaire\n-/"}

Raw output

{"env": 0}

1.3 Importer Mathlib

Les imports Mathlib suivent une hiérarchie : Mathlib.Data.Nat.Prime pour les nombres premiers, Mathlib.Algebra.Ring.Basic pour les anneaux, etc.

/-!
## Imports Mathlib typiques (a utiliser dans un projet avec Mathlib)

Dans un projet avec Mathlib installe, on utiliserait :
- `import Mathlib.Tactic` : Toutes les tactiques (ring, linarith, norm_num)
- `import Mathlib.Data.Nat.Prime` : Nombres premiers
- `import Mathlib.Algebra.Ring.Basic` : Structures d'anneaux
- `import Mathlib.Analysis.SpecialFunctions.Log.Basic` : Logarithmes

**Note importante** : Ce notebook s'exécute dans un environnement Jupyter avec
lean4_jupyter, sans acces direct a Mathlib. Les exemples Mathlib sont documentes
en commentaires. Pour les exécuter, utilisez un projet Lake avec Mathlib.

Les tactiques disponibles dans Lean de base (sans Mathlib) incluent :
- `omega` : Arithmetique de Presburger (entiers avec +, -, <, <=)
- `simp` : Simplification automatique
- `rfl` : Reflexivite
- `decide` : Propositions decidables (tactique Lean, sans accent)
-/

-- Vérification que l'environnement Lean fonctionne
#check Nat
#check @Nat.add_comm

/-!

## Imports Mathlib typiques (a utiliser dans un projet avec Mathlib)

Dans un projet avec Mathlib installe, on utiliserait :

- `import Mathlib.Tactic` : Toutes les tactiques (ring, linarith, norm_num)

- `import Mathlib.Data.Nat.Prime` : Nombres premiers

- `import Mathlib.Algebra.Ring.Basic` : Structures d'anneaux

- `import Mathlib.Analysis.SpecialFunctions.Log.Basic` : Logarithmes

**Note importante** : Ce notebook s'exécute dans un environnement Jupyter avec

lean4_jupyter, sans acces direct a Mathlib. Les exemples Mathlib sont documentes

en commentaires. Pour les exécuter, utilisez un projet Lake avec Mathlib.

Les tactiques disponibles dans Lean de base (sans Mathlib) incluent :

- `omega` : Arithmetique de Presburger (entiers avec +, -, <, <=)

- `simp` : Simplification automatique

- `rfl` : Reflexivite

- `decide` : Propositions decidables (tactique Lean, sans accent)

-/

-- Vérification que l'environnement Lean fonctionne

#check Nat Nat : Type

#check @Nat.add_comm Nat.add_comm : ∀ (n m : Nat), n + m = m + n

--% env 1

Raw input

{"cmd": "/-!\n## Imports Mathlib typiques (a utiliser dans un projet avec Mathlib)\n\nDans un projet avec Mathlib installe, on utiliserait :\n- `import Mathlib.Tactic` : Toutes les tactiques (ring, linarith, norm_num)\n- `import Mathlib.Data.Nat.Prime` : Nombres premiers\n- `import Mathlib.Algebra.Ring.Basic` : Structures d'anneaux\n- `import Mathlib.Analysis.SpecialFunctions.Log.Basic` : Logarithmes\n\n**Note importante** : Ce notebook s'ex\u00e9cute dans un environnement Jupyter avec\nlean4_jupyter, sans acces direct a Mathlib. Les exemples Mathlib sont documentes\nen commentaires. Pour les ex\u00e9cuter, utilisez un projet Lake avec Mathlib.\n\nLes tactiques disponibles dans Lean de base (sans Mathlib) incluent :\n- `omega` : Arithmetique de Presburger (entiers avec +, -, <, <=)\n- `simp` : Simplification automatique\n- `rfl` : Reflexivite\n- `decide` : Propositions decidables (tactique Lean, sans accent)\n-/\n\n-- V\u00e9rification que l'environnement Lean fonctionne\n#check Nat\n#check @Nat.add_comm", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 22, "column": 0},
   "endPos": {"line": 22, "column": 6},
   "data": "Nat : Type"},
  {"severity": "info",
   "pos": {"line": 23, "column": 0},
   "endPos": {"line": 23, "column": 6},
   "data": "Nat.add_comm : ∀ (n m : Nat), n + m = m + n"}],
 "env": 1}

Pourquoi ces imports ouvrent toute la bibliothèque

La cellule de gauche importe les espaces de noms fondamentaux de Mathlib : Mathlib.Tactic (les tactiques ring, linarith, field_simp…), Mathlib.Data.Nat.Basic (lemmes sur Nat), Mathlib.Algebra (structures algébriques). En Lean 4, un import n’est pas un #include C : c’est la déclaration qu’on veut accéder à un module compilé. Sans Mathlib.Tactic, la tactique ring n’existe pas ; sans Mathlib.Data.Nat, des lemmes comme Nat.add_comm doivent être prouvés à la main.

Le pont vers la partie haute : Lean-12 (sensibilité de Huang) importe Mathlib.Analysis et Mathlib.Data.Complex.Basic pour manipuler les dérivées et sommes partielles. Lean-14 (Finiteness) importe Mathlib.Topology pour les notions de compacité. La hiérarchie d’imports de Mathlib est ce qui rend ces preuves avancées possibles sans réinventer l’analyse.

2. Structure de Mathlib4

2.1 Organisation des modules

Mathlib est organise en namespaces thematiques :

Namespace	Contenu	Exemples
`Mathlib.Data`	Structures de données	List, Set, Finset, Multiset
`Mathlib.Algebra`	Structures algébriques	Group, Ring, Field, Module
`Mathlib.Order`	Relations d’ordre	Lattice, Complète lattice
`Mathlib.Topology`	Topologie générale	Espaces topologiques, compacite
`Mathlib.Analysis`	Analyse réelle/complexe	Limites, dérivées, intégrales
`Mathlib.NumberTheory`	Théorie des nombres	Primalite, congruences, Legendre
`Mathlib.Logic`	Logique avancee	Logique classique, cardinalite
`Mathlib.Tactic`	Tactiques Mathlib	ring, linarith, omega, polyrith

2.2 Hiérarchie de structures algébriques

Mathlib définit une hiérarchie riche de structures algébriques :

Semigroup -> Monoid -> Group
    |           |         |
    v           v         v
CommSemigroup -> CommMonoid -> CommGroup
    |           |         |
    v           v         v
Semiring  ->   Ring   ->  Field

Cette hiérarchie utilise les typeclasses de Lean pour l’inference automatique.

-- Exemple conceptuel de typeclass (syntaxe simplifiee)
-- class Monoid (M : Type*) extends One M, Mul M where
--   one_mul : forall a : M, 1 * a = a
--   mul_one : forall a : M, a * 1 = a
--   mul_assoc : forall a b c : M, (a * b) * c = a * (b * c)

-- Nat est automatiquement un Monoid additif et multiplicatif
#check @Nat.add_comm      -- Commutativity de l'addition
#check @Nat.mul_assoc     -- Associativite de la multiplication

-- Exemple conceptuel de typeclass (syntaxe simplifiee)

-- class Monoid (M : Type*) extends One M, Mul M where

--   one_mul : forall a : M, 1 * a = a

--   mul_one : forall a : M, a * 1 = a

--   mul_assoc : forall a b c : M, (a * b) * c = a * (b * c)

-- Nat est automatiquement un Monoid additif et multiplicatif

#check @Nat.add_comm      -- Commutativity de l'addition Nat.add_comm : ∀ (n m : Nat), n + m = m + n

#check @Nat.mul_assoc     -- Associativite de la multiplication Nat.mul_assoc : ∀ (n m k : Nat), n * m * k = n * (m * k)

--% env 2

Raw input

{"cmd": "-- Exemple conceptuel de typeclass (syntaxe simplifiee)\n-- class Monoid (M : Type*) extends One M, Mul M where\n--   one_mul : forall a : M, 1 * a = a\n--   mul_one : forall a : M, a * 1 = a\n--   mul_assoc : forall a b c : M, (a * b) * c = a * (b * c)\n\n-- Nat est automatiquement un Monoid additif et multiplicatif\n#check @Nat.add_comm      -- Commutativity de l'addition\n#check @Nat.mul_assoc     -- Associativite de la multiplication", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data": "Nat.add_comm : ∀ (n m : Nat), n + m = m + n"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data": "Nat.mul_assoc : ∀ (n m k : Nat), n * m * k = n * (m * k)"}],
 "env": 2}

Hiérarchie des typeclasses — l’algèbre en couches

Mathlib structure les mathématiques via des typeclasses : Semiring, Ring, CommRing, Field forment une chaîne où chaque niveau ajoute une propriété. Un théorème prouvé sur Semiring (le niveau le plus bas) s’applique automatiquement à Nat, Int, Rat, Real, Complex — c’est la réutilisabilité. À l’inverse, un théorème sur Field ne s’applique pas à Nat (qui n’est qu’un Semiring/CommSemiring).

Pourquoi cette architecture : éviter de prouver add_comm séparément pour chaque type. La typeclass capture l’abstraction commune.
Comment lire une signature theorem foo {R : Type*} [Ring R] ... — le [Ring R] est une instance : Lean cherche automatiquement une structure de Ring sur R. Si R = Int, l’instance est trouvée ; si R = Nat, Lean refuse (pas un Ring).
Pont : Lean-14 (Finiteness) utilise [TopologicalSpace X] et [CompactSpace X] de la même manière — les typeclasses topologiques remplacent les algébriques.

3. Tactiques Mathlib Essentielles

Mathlib fournit des tactiques puissantes qui automatisent de nombreuses preuves. Ces tactiques ne sont pas dans Lean de base mais deviennent indispensables pour les mathematiques serieuses.

3.1 `ring` : Algebre polynomiale

La tactique ring resout automatiquement les égalités dans les anneaux (commutatifs ou non).

-- Exemples avec ring (necessite Mathlib.Tactic)
-- Ces exemples fonctionnent dans un projet avec Mathlib installe

-- Identite remarquable
-- example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

-- Factorisation
-- example (a b : Int) : a^2 - b^2 = (a + b) * (a - b) := by ring

-- Expression complexe
-- example (x y z : Int) : 
--   (x + y + z)^2 = x^2 + y^2 + z^2 + 2*x*y + 2*x*z + 2*y*z := by ring

-- Pour Nat (sans Mathlib), on peut utiliser des lemmes manuellement
-- Voici une version simplifiee demontrant le concept
theorem double_times (a : Nat) : a + a = 2 * a := by
  simp [Nat.two_mul]

-- Avec Mathlib installe, on prouverait directement :
-- theorem square_expand (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring

-- Exemples avec ring (necessite Mathlib.Tactic)

-- Ces exemples fonctionnent dans un projet avec Mathlib installe

-- Identite remarquable

-- example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

-- Factorisation

-- example (a b : Int) : a^2 - b^2 = (a + b) * (a - b) := by ring

-- Expression complexe

-- example (x y z : Int) :

--   (x + y + z)^2 = x^2 + y^2 + z^2 + 2*x*y + 2*x*z + 2*y*z := by ring

-- Pour Nat (sans Mathlib), on peut utiliser des lemmes manuellement

-- Voici une version simplifiee demontrant le concept

theorem double_times (a : Nat) : a + a = 2 * a := by

  simp [Nat.two_mul]

-- Avec Mathlib installe, on prouverait directement :

-- theorem square_expand (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring

--% env 3

Raw input

{"cmd": "-- Exemples avec ring (necessite Mathlib.Tactic)\n-- Ces exemples fonctionnent dans un projet avec Mathlib installe\n\n-- Identite remarquable\n-- example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring\n\n-- Factorisation\n-- example (a b : Int) : a^2 - b^2 = (a + b) * (a - b) := by ring\n\n-- Expression complexe\n-- example (x y z : Int) : \n--   (x + y + z)^2 = x^2 + y^2 + z^2 + 2*x*y + 2*x*z + 2*y*z := by ring\n\n-- Pour Nat (sans Mathlib), on peut utiliser des lemmes manuellement\n-- Voici une version simplifiee demontrant le concept\ntheorem double_times (a : Nat) : a + a = 2 * a := by\n  simp [Nat.two_mul]\n\n-- Avec Mathlib installe, on prouverait directement :\n-- theorem square_expand (a b : Nat) : (a + b) * (a + b) = a*a + 2*a*b + b*b := by ring", "env": 2}

Raw output

{"env": 3}

`ring` — la tactique de l’anneau commutatif

ring décide l’égalité de deux expressions polynomiales sur un anneau commutatif en normalisant les deux côtés vers une forme canonique (développer, réordonner par degrés). Elle est complète sur sa fragment : soit ça se prouve, soit ça échoue (jamais de faux négatifs dans le fragment anneau).

Quand ring vs omega : ring traite les égalités polynomiales ((a+b)^2 = a^2 + 2ab + b^2) ; omega traite les inégalités et égalités linéaires sur Nat/Int. Sur x^2 = x*x, ring réussit, omega échoue (non-linéaire). Sur x + y = y + x, les deux réussissent.
Limite : ring ne sait PAS factoriser ou utiliser des hypothèses hétérogènes. Pour (a+b)*(a-b) = a^2 - b^2, ring réussit ; pour prouver ça à partir de h1 : a^2 - b^2 = c, il faut linarith ou du manuel.
Pont : Lean-12 (sensibilité) n’utilise presque jamais ring directement — ses égalités portent sur des sommes indicées et des normes, pas des polynômes plats. Mais ring sous-tend simp et norm_num qui, eux, apparaissent partout.

Pour aller plus loin — Surviving proofs, Why Do We Care About Proofs? (29/08/2026) Sheydvasser, à l’article 0, insiste : une preuve n’est pas seulement un certificat, c’est une stratégie qui éclaire. Ici, le choix entre ring et omega n’est pas qu’une question de performance — c’est une décision tactique qui dépend du fragment d’arithmétique qu’on manipule (anneau commutatif clos vs arithmétique linéaire sur les entiers). Échec de l’un, succès de l’autre : c’est exactement le réseau de concepts qu’elle recommande d’expliciter, plutôt que de tester au hasard. Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/why-do-we-care-about-proofs Archivé : G:DriveIA-Proves-Surviving-Proofs\2026-08-29_why-do-we-care-about-proofs.html

3.2 `linarith` : Arithmetique linéaire

La tactique linarith resout automatiquement les inégalités linéaires sur les nombres reels, rationnels ou entiers. Elle combine les hypotheses pour trouver une contradiction.

Pourquoi `linarith` existe (et quand l’utiliser)

linarith est l’implémentation Lean de l’algorithme de Fourier-Motzkin : élimination des variables par combinaisons linéaires d’inégalités. C’est une décision procedure complète pour le fragment linéaire (additions, multiplications par scalaires, comparaisons) sur les corps ordonnes archimediens.

Module Mathlib : Mathlib.Tactic.Linarith – définit linarith et nlinarith. nlinarith ajoute une passe de non-linearite (termes quadratiques) avant Fourier-Motzkin.

Regle pratique : - Inégalités entières (Nat/Int) : préférer omega (décideur Presburger, plus expressif, gere la modularite). - Inégalités réelles (Real) ou rationnelles (Rat) : linarith est la seule option (omega ne couvre pas les reels). - Non-linearite : nlinarith tente de detecter des termes quadratiques avant la passe linéaire.

Ou cette tactique porte : Lean-12 (sensibilité de Huang) l’utilise systématiquement pour borner les sommes partielles de la forme ‖Σ x_i‖ ≤ Σ ‖x_i‖ (norme triangulaire linéaire). C’est la tactique standard des preuves d’analyse bornee en Lean.

-- Exemples avec linarith (Mathlib.Tactic)

-- Inégalité simple
-- example (x : Int) (h : x > 5) : x >= 5 := by linarith

-- Combinaison d'hypotheses
-- example (x y : Int) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by linarith

-- Système d'inégalités
-- example (a b c : Int) (h1 : a + b > c) (h2 : b + c > a) (h3 : c + a > b) :
--   a + b + c > 0 := by linarith

-- Version avec omega (disponible dans Lean de base pour Nat/Int)
theorem ineq_example (x y : Nat) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by
  omega

-- Exemples avec linarith (Mathlib.Tactic)

-- Inégalité simple

-- example (x : Int) (h : x > 5) : x >= 5 := by linarith

-- Combinaison d'hypotheses

-- example (x y : Int) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by linarith

-- Système d'inégalités

-- example (a b c : Int) (h1 : a + b > c) (h2 : b + c > a) (h3 : c + a > b) :

--   a + b + c > 0 := by linarith

-- Version avec omega (disponible dans Lean de base pour Nat/Int)

theorem ineq_example (x y : Nat) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by

  omega

--% env 4

Raw input

{"cmd": "-- Exemples avec linarith (Mathlib.Tactic)\n\n-- In\u00e9galit\u00e9 simple\n-- example (x : Int) (h : x > 5) : x >= 5 := by linarith\n\n-- Combinaison d'hypotheses\n-- example (x y : Int) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by linarith\n\n-- Syst\u00e8me d'in\u00e9galit\u00e9s\n-- example (a b c : Int) (h1 : a + b > c) (h2 : b + c > a) (h3 : c + a > b) :\n--   a + b + c > 0 := by linarith\n\n-- Version avec omega (disponible dans Lean de base pour Nat/Int)\ntheorem ineq_example (x y : Nat) (h1 : x <= y) (h2 : y <= x + 3) : y - x <= 3 := by\n  omega", "env": 3}

Raw output

{"env": 4}

`linarith` — l’arithmétique linéaire réelle

linarith décide les inégalités linéaires sur Int, Rat, Real via l’algorithme de Fourier-Motzkin : combiner des hypothèses d’inégalité pour prouver une cible d’inégalité. Limité au fragment linéaire (pas de produits de variables).

linarith vs omega : omega couvre Nat/Int avec modularité (Presburger, plus expressif sur les entiers) ; linarith couvre tous les corps ordonnés (Real) mais sans modularité. Règle pratique : entiers → omega ; réels → linarith.
Combinaison d’hypothèses : linarith trouve automatiquement la combinaison linéaire des h1, h2, h3 qui implique la cible. Pas besoin de have intermédiaires.
Pont : Lean-12 (sensibilité) utilise linarith et nlinarith pour borner les sommes partielles — les inégalités de norme triangulaire ‖Σ x_i‖ ≤ Σ ‖x_i‖ sont linéaires en les normes.

3.3 `omega` : Arithmetique Presburger

La tactique omega est un décideur complet pour l’arithmetique de Presburger (entiers avec +, -, comparaisons). Plus puissante que linarith pour les entiers.

-- omega est disponible dans Lean de base pour Nat et Int

-- Égalités et inégalités
theorem omega_demo1 (n m : Nat) : n + m = m + n := by omega

theorem omega_demo2 (n : Nat) (h : n > 0) : n >= 1 := by omega

-- Systemes complexes
theorem omega_complex (a b c : Int)
  (h1 : a + b = c) (h2 : a - b = 0) : 2 * a = c := by omega

-- Divisibilite (modulo)
-- theorem div_mod (n : Nat) : n = n / 2 * 2 + n % 2 := by omega

-- omega est disponible dans Lean de base pour Nat et Int

-- Égalités et inégalités

theorem omega_demo1 (n m : Nat) : n + m = m + n := by omega

theorem omega_demo2 (n : Nat) (h : n > 0) : n >= 1 := by omega

-- Systemes complexes

theorem omega_complex (a b c : Int)

  (h1 : a + b = c) (h2 : a - b = 0) : 2 * a = c := by omega

-- Divisibilite (modulo)

-- theorem div_mod (n : Nat) : n = n / 2 * 2 + n % 2 := by omega

--% env 5

Raw input

{"cmd": "-- omega est disponible dans Lean de base pour Nat et Int\n\n-- \u00c9galit\u00e9s et in\u00e9galit\u00e9s\ntheorem omega_demo1 (n m : Nat) : n + m = m + n := by omega\n\ntheorem omega_demo2 (n : Nat) (h : n > 0) : n >= 1 := by omega\n\n-- Systemes complexes\ntheorem omega_complex (a b c : Int)\n  (h1 : a + b = c) (h2 : a - b = 0) : 2 * a = c := by omega\n\n-- Divisibilite (modulo)\n-- theorem div_mod (n : Nat) : n = n / 2 * 2 + n % 2 := by omega", "env": 4}

Raw output

{"env": 5}

`omega` — l’arithmétique de Presburger

omega décide la théorie de Presburger : égalités, inégalités, et divisibilité (modularité) sur Nat et Int. C’est la tactique la plus puissante du fragment arithmétique entier — complète et décidable. Disponible dans Lean de base (sans Mathlib).

Pourquoi omega est le couteau suisse des entiers : elle gère les systèmes d’équations, les inégalités combinées, et même n % 2 = .... Toute inégalité entière linéaire se tente d’abord par omega.
Limite — non-linéaire : a * b = b * a (produit de variables) échoue sur omega. Il faut mul_comm ou ring.
Pont : Lean-14 (Finiteness) utilise omega pour les bornes sur les tailles finies (cardinalité d’un Finset, indices Fin n). Lean-16b (Game of Life) utilise omega pour les inégalités de coordonnées de grille.

3.4 `norm_num` : Calcul numérique

La tactique norm_num évalue les expressions numériques et vérifie les propriétés calculables (primalite, divisibilite, etc.). Indispensable pour les assertions concretes.

-- Exemples avec norm_num (Mathlib.Tactic.NormNum)

-- Calculs simples
-- example : (2 : Nat) + 2 = 4 := by norm_num
-- example : (123 : Nat) * 456 = 56088 := by norm_num

-- Primalite
-- example : Nat.Prime 17 := by norm_num
-- example : ¬ Nat.Prime 15 := by norm_num

-- Comparaisons
-- example : (100 : Nat) < 200 := by norm_num

-- Sans Mathlib, on utilise decide ou rfl
theorem calc_example : 2 + 2 = 4 := by rfl
theorem compare_example : 5 < 10 := by decide

-- Exemples avec norm_num (Mathlib.Tactic.NormNum)

-- Calculs simples

-- example : (2 : Nat) + 2 = 4 := by norm_num

-- example : (123 : Nat) * 456 = 56088 := by norm_num

-- Primalite

-- example : Nat.Prime 17 := by norm_num

-- example : ¬ Nat.Prime 15 := by norm_num

-- Comparaisons

-- example : (100 : Nat) < 200 := by norm_num

-- Sans Mathlib, on utilise decide ou rfl

theorem calc_example : 2 + 2 = 4 := by rfl

theorem compare_example : 5 < 10 := by decide

--% env 6

Raw input

{"cmd": "-- Exemples avec norm_num (Mathlib.Tactic.NormNum)\n\n-- Calculs simples\n-- example : (2 : Nat) + 2 = 4 := by norm_num\n-- example : (123 : Nat) * 456 = 56088 := by norm_num\n\n-- Primalite\n-- example : Nat.Prime 17 := by norm_num\n-- example : \u00ac Nat.Prime 15 := by norm_num\n\n-- Comparaisons\n-- example : (100 : Nat) < 200 := by norm_num\n\n-- Sans Mathlib, on utilise decide ou rfl\ntheorem calc_example : 2 + 2 = 4 := by rfl\ntheorem compare_example : 5 < 10 := by decide", "env": 5}

Raw output

{"env": 6}

`norm_num` — le calcul numérique exact

norm_num évalue les expressions numériques closes : 2 + 2 = 4, 123 * 456 = 56088, Nat.Prime 17. Contrairement à rfl (qui utilise la définition), norm_num utilise des algorithmes efficaces (équations de Hadamard pour la multiplication, certificats de primalité). Sans Mathlib, decide remplace norm_num mais est beaucoup plus lent.

norm_num vs rfl vs decide : rfl prouve par réduction définitionnelle (rapide mais limité) ; decide teste exhaustivement (lent) ; norm_num normalise efficacement (rapide et puissant). Pour 2 + 2 = 4, les trois marchent ; pour Nat.Prime 17, seul norm_num/decide.
Cas d’usage typique : vérifier une valeur numérique concrète dans une preuve (un seuil, une borne). norm_num ferme le but en une ligne.
Pont : Lean-12 (sensibilité) utilise norm_num pour vérifier les constantes dans les bornes (ex. k ≤ 2^10 fermé par norm_num).

3.5 `field_simp` : Simplification dans les corps

field_simp simplifie les expressions avec divisions et fractions.

Pourquoi `field_simp` est necessaire (les `simp` classiques echouent)

simp (la simplification par defaut) ne sait pas manipuler les fractions : il ne peut pas prouver a / b * b = a parce que cette égalité n’est pas une reecriture structurelle, elle exige d’inverser la multiplication (passe par l’inverse dans le corps). field_simp ajoute cette capacite : il transforme les expressions en fractions en produits d’inverses, puis reecrit.

Module Mathlib : Mathlib.Tactic.FieldSimp – la tactique opere sur tout type muni d’une structure de corps divise (DivisionRing / Field), c’est-a-dire un anneau avec inverse multiplicatif : Rat, Real, Complex. Sans Mathlib, les fractions restent des opérations opaques.

Distinction : - simp : reecrit via des égalités definies @[simp]. Rapide mais ignore les fractions. - field_simp : ajoute la passe fraction + inverse. Plus lent mais prouve les égalités de fractions en une ligne. - ring : utile apres field_simp pour finir la normalisation algébrique du résultat.

Quand l’utiliser : toute expression contenant / ou ·⁻¹ qui devrait se simplifier. Le pattern typique est field_simp; ring – field_simp ramene les fractions a un denominateur commun, ring normalise le polynome final.

Ou cette tactique porte : Lean-12 (sensibilité) et Lean-14 (Finiteness) manipulent des ratios de cardinalite et des quotients ; field_simp y intervient systématiquement quand la cible contient une division.

/-!
## Exemples avec field_simp (Mathlib.Tactic.FieldSimp)

La tactique `field_simp` simplifie les expressions avec divisions et fractions.
Elle necessite Mathlib.

**Avec Mathlib installe :**
```lean
-- Fractions
example (a b : Rat) (hb : b ≠ 0) : a / b * b = a := by field_simp

-- Addition de fractions
example (a b c : Rat) (hb : b ≠ 0) (hc : c ≠ 0) :
  a / b + a / c = a * (b + c) / (b * c) := by field_simp; ring

-- Simplification complexe
example (x : Real) (hx : x ≠ 0) : (x + 1) / x - 1 / x = 1 := by
  field_simp
  ring
```
-/

-- Sans Mathlib, on peut travailler avec les rationnels de Lean de base
-- mais les simplifications de fractions sont plus limitees
#check @Rat.add_comm
#check @Rat.mul_comm

/-!

## Exemples avec field_simp (Mathlib.Tactic.FieldSimp)

La tactique `field_simp` simplifie les expressions avec divisions et fractions.

Elle necessite Mathlib.

**Avec Mathlib installe :**

```lean

-- Fractions

example (a b : Rat) (hb : b ≠ 0) : a / b * b = a := by field_simp

-- Addition de fractions

example (a b c : Rat) (hb : b ≠ 0) (hc : c ≠ 0) :

  a / b + a / c = a * (b + c) / (b * c) := by field_simp; ring

-- Simplification complexe

example (x : Real) (hx : x ≠ 0) : (x + 1) / x - 1 / x = 1 := by

  field_simp

  ring

```

-/

-- Sans Mathlib, on peut travailler avec les rationnels de Lean de base

-- mais les simplifications de fractions sont plus limitees

#check @Rat.add_comm Rat.add_comm : ∀ (a b : Rat), a + b = b + a

#check @Rat.mul_comm Rat.mul_comm : ∀ (a b : Rat), a * b = b * a

--% env 7

Raw input

{"cmd": "/-!\n## Exemples avec field_simp (Mathlib.Tactic.FieldSimp)\n\nLa tactique `field_simp` simplifie les expressions avec divisions et fractions.\nElle necessite Mathlib.\n\n**Avec Mathlib installe :**\n```lean\n-- Fractions\nexample (a b : Rat) (hb : b \u2260 0) : a / b * b = a := by field_simp\n\n-- Addition de fractions\nexample (a b c : Rat) (hb : b \u2260 0) (hc : c \u2260 0) :\n  a / b + a / c = a * (b + c) / (b * c) := by field_simp; ring\n\n-- Simplification complexe\nexample (x : Real) (hx : x \u2260 0) : (x + 1) / x - 1 / x = 1 := by\n  field_simp\n  ring\n```\n-/\n\n-- Sans Mathlib, on peut travailler avec les rationnels de Lean de base\n-- mais les simplifications de fractions sont plus limitees\n#check @Rat.add_comm\n#check @Rat.mul_comm", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 25, "column": 0},
   "endPos": {"line": 25, "column": 6},
   "data": "Rat.add_comm : ∀ (a b : Rat), a + b = b + a"},
  {"severity": "info",
   "pos": {"line": 26, "column": 0},
   "endPos": {"line": 26, "column": 6},
   "data": "Rat.mul_comm : ∀ (a b : Rat), a * b = b * a"}],
 "env": 7}

3.6 `polyrith` : Certificats polynomiaux

polyrith trouve automatiquement des preuves polynomiales en interrogeant Sage (système de calcul formel).

Pourquoi `polyrith` complète `omega` et `ring`

Les tactiques arithmetiques ont chacune leur frontiere : - omega : arithmetique linéaire sur Nat/Int (Presburger). Complet pour ce fragment, refuse le non-linéaire. - ring : égalités algébriques sur les anneaux. Complet pour les polynomes, refuse les hypotheses heterogenes (un mix de contraintes h1 : a + b = 4 et h2 : a - b = 2 necessite une resolution système). - polyrith : systemes d’égalités polynomiales avec hypotheses. Il transforme les contraintes en un système linéaire sur les coefficients et interroge Sage (système de calcul formel) pour trouver un certificat.

Module Mathlib : Mathlib.Tactic.Polyrith – la tactique envoie la cible et les hypotheses a Sage via une interface externe, puis vérifie le certificat recu.

Limite pratique : polyrith necessite que Sage soit installe et accessible depuis Lean. Sans Sage, la tactique echoue avec un message d’erreur externe – c’est l’une des rares tactiques Mathlib qui depend d’un outil extérieur. En pratique, dans un projet Lake, on declare Sage comme require sage dans lakefile.lean.

Quand l’utiliser : preuve de la forme theorem foo (a b c : Int) (h1 : ...) (h2 : ...) : cible := by polyrith. C’est le couteau suisse des systemes d’équations polynomiales avec hypotheses.

Ou cette tactique porte : Lean-12 (sensibilité) l’utilise pour les bornes polynomiales dans les analyses de stabilite, Lean-16b (Game of Life) pour les invariants de regles de transition polynomiales.

/-!
## Exemples avec polyrith (Mathlib.Tactic.Polyrith)

La tactique `polyrith` trouve automatiquement des preuves polynomiales
en interrogeant **Sage** (système de calcul formel externe).

**Avec Mathlib installe et Sage disponible :**
```lean
-- Égalité polynomiale non triviale
example (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by polyrith

-- Système d'équations
example (x y : Rat) (h1 : 2*x + 3*y = 7) (h2 : x - y = 1) : 
  x = 2 := by polyrith
```
-/

-- Sans polyrith, on peut resoudre manuellement avec omega pour les entiers
theorem systeme_lineaire (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by
  omega

theorem systeme_lineaire2 (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : b = 1 := by
  omega

/-!

## Exemples avec polyrith (Mathlib.Tactic.Polyrith)

La tactique `polyrith` trouve automatiquement des preuves polynomiales

en interrogeant **Sage** (système de calcul formel externe).

**Avec Mathlib installe et Sage disponible :**

```lean

-- Égalité polynomiale non triviale

example (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by polyrith

-- Système d'équations

example (x y : Rat) (h1 : 2*x + 3*y = 7) (h2 : x - y = 1) :

  x = 2 := by polyrith

```

-/

-- Sans polyrith, on peut resoudre manuellement avec omega pour les entiers

theorem systeme_lineaire (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by

  omega

theorem systeme_lineaire2 (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : b = 1 := by

  omega

--% env 8

Raw input

{"cmd": "/-!\n## Exemples avec polyrith (Mathlib.Tactic.Polyrith)\n\nLa tactique `polyrith` trouve automatiquement des preuves polynomiales\nen interrogeant **Sage** (syst\u00e8me de calcul formel externe).\n\n**Avec Mathlib installe et Sage disponible :**\n```lean\n-- \u00c9galit\u00e9 polynomiale non triviale\nexample (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by polyrith\n\n-- Syst\u00e8me d'\u00e9quations\nexample (x y : Rat) (h1 : 2*x + 3*y = 7) (h2 : x - y = 1) : \n  x = 2 := by polyrith\n```\n-/\n\n-- Sans polyrith, on peut resoudre manuellement avec omega pour les entiers\ntheorem systeme_lineaire (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : a = 3 := by\n  omega\n\ntheorem systeme_lineaire2 (a b : Int) (h1 : a + b = 4) (h2 : a - b = 2) : b = 1 := by\n  omega", "env": 7}

Raw output

{"env": 8}

4. Exemples de Théorèmes Mathlib

4.1 Théorie des nombres

/-!
## Theorie des nombres avec Mathlib

Avec `import Mathlib.Data.Nat.Prime`, on accede a :
- `Nat.Prime` : Définition de nombre premier
- `Nat.Prime.two_le` : p premier => p >= 2  
- `Nat.Prime.one_lt` : p premier => 1 < p
- `Nat.minFac_prime` : Plus petit facteur premier
- `Nat.exists_infinite_primes` : Théorème d'Euclide (infinite de premiers)

**Exemple avec norm_num :**
```lean
theorem prime_17 : Nat.Prime 17 := by norm_num
```
-/

-- Sans Mathlib, on peut définir et utiliser des predicats simples sur les nombres
def estPair (n : Nat) : Prop := n % 2 = 0
def estImpair (n : Nat) : Prop := n % 2 = 1

-- Preuves basiques
theorem deux_pair : estPair 2 := by rfl
theorem trois_impair : estImpair 3 := by rfl
theorem seize_pair : estPair 16 := by rfl

-- Lemmes sur la parite avec omega
theorem pair_plus_pair (a b : Nat) (ha : estPair a) (hb : estPair b) : estPair (a + b) := by
  unfold estPair at *
  omega

/-!

## Theorie des nombres avec Mathlib

Avec `import Mathlib.Data.Nat.Prime`, on accede a :

- `Nat.Prime` : Définition de nombre premier

- `Nat.Prime.two_le` : p premier => p >= 2

- `Nat.Prime.one_lt` : p premier => 1 < p

- `Nat.minFac_prime` : Plus petit facteur premier

- `Nat.exists_infinite_primes` : Théorème d'Euclide (infinite de premiers)

**Exemple avec norm_num :**

```lean

theorem prime_17 : Nat.Prime 17 := by norm_num

```

-/

-- Sans Mathlib, on peut définir et utiliser des predicats simples sur les nombres

def estPair (n : Nat) : Prop := n % 2 = 0

def estImpair (n : Nat) : Prop := n % 2 = 1

-- Preuves basiques

theorem deux_pair : estPair 2 := by rfl

theorem trois_impair : estImpair 3 := by rfl

theorem seize_pair : estPair 16 := by rfl

-- Lemmes sur la parite avec omega

theorem pair_plus_pair (a b : Nat) (ha : estPair a) (hb : estPair b) : estPair (a + b) := by

  unfold estPair at *

  omega

--% env 9

Raw input

{"cmd": "/-!\n## Theorie des nombres avec Mathlib\n\nAvec `import Mathlib.Data.Nat.Prime`, on accede a :\n- `Nat.Prime` : D\u00e9finition de nombre premier\n- `Nat.Prime.two_le` : p premier => p >= 2  \n- `Nat.Prime.one_lt` : p premier => 1 < p\n- `Nat.minFac_prime` : Plus petit facteur premier\n- `Nat.exists_infinite_primes` : Th\u00e9or\u00e8me d'Euclide (infinite de premiers)\n\n**Exemple avec norm_num :**\n```lean\ntheorem prime_17 : Nat.Prime 17 := by norm_num\n```\n-/\n\n-- Sans Mathlib, on peut d\u00e9finir et utiliser des predicats simples sur les nombres\ndef estPair (n : Nat) : Prop := n % 2 = 0\ndef estImpair (n : Nat) : Prop := n % 2 = 1\n\n-- Preuves basiques\ntheorem deux_pair : estPair 2 := by rfl\ntheorem trois_impair : estImpair 3 := by rfl\ntheorem seize_pair : estPair 16 := by rfl\n\n-- Lemmes sur la parite avec omega\ntheorem pair_plus_pair (a b : Nat) (ha : estPair a) (hb : estPair b) : estPair (a + b) := by\n  unfold estPair at *\n  omega", "env": 8}

Raw output

{"env": 9}

4.2 Algebre

La cellule de gauche explore l’algebre de base de Mathlib en important Mathlib.Algebra.Group.Basic – le module ou vivent les lemmes fondamentaux des structures multiplicatives et additives (mul_one, one_mul, mul_assoc, add_zero, zero_add, add_assoc, left_distrib, right_distrib). Ces noms suivent une convention stricte : Namespace.Concept.property – Nat.add_comm est la commutativite de l’addition sur Nat, Monoid.mul_assoc serait l’associativite sur un monoide quelconque. Le nom EST la specification, ce qui rend Loogle et Moogle efficaces pour la recherche.

Pourquoi `Group.Basic` est le bon point d’entrée

Couverture maximale : Group.Basic regroupe les lemmes valables sur tout type ayant une structure de groupe ou de monoide – donc sur Int, Rat, Real, Complex, matrices, polynomes, etc. Un théorème prouvé dans ce module s’applique automatiquement partout ou la typeclass est resolue.
Trois familles distinctes : (a) Monoid = mul_one, one_mul, mul_assoc ; (b) Group ajoute mul_inv_cancel (inverse) ; (c) Ring ajoute add_mul, mul_add, neg_add_cancel. La hierarchie de typeclasses empile ces obligations.
Pont direct avec Lean-14 (Finiteness) : ce notebook utilise Finset.card_mul, Finset.card_product, lemmes de comptage qui reposent tous sur les propriétés de monoide de Nat. Sans Group.Basic, Lean ne saurait pas que card (s × t) = card s * card t.

Strategie de lecture du bloc code

Au lieu de prouver n + m = m + n a la main, simp [Nat.add_comm] ou exact Nat.add_comm n m resout en une ligne. La majorite des identites algébriques postees dans le bloc gauche ont deja un lemme Mathlib – le travail consiste a les trouver (via Loogle, Moogle, ou exact?), pas a les reinventer. C’est une inversion pedagogique : on apprend Mathlib en lisant son catalogue, pas en prouvant ce qu’il sait deja.

/-!
## Algebre avec Mathlib

Avec `import Mathlib.Algebra.Group.Basic`, on accede aux propriétés generiques :

**Groupes :**
- `mul_one` : a * 1 = a
- `one_mul` : 1 * a = a  
- `mul_assoc` : (a * b) * c = a * (b * c)
- `mul_inv_cancel` : a * a⁻¹ = 1

**Anneaux :**
- `add_mul` : (a + b) * c = a * c + b * c
- `mul_add` : a * (b + c) = a * b + a * c
- `neg_add_cancel` : -a + a = 0

Ces théorèmes s'appliquent a TOUS les types avec la structure adequate
(Int, Rat, Real, Complex, matrices, polynomes, etc.).
-/

-- Sans Mathlib, on a les propriétés specifiques aux types concrets
-- Voici quelques exemples avec Nat et Int

-- Addition : propriétés fondamentales
#check @Nat.add_assoc    -- (a + b) + c = a + (b + c)
#check @Nat.add_comm     -- a + b = b + a
#check @Nat.add_zero     -- a + 0 = a
#check @Nat.zero_add     -- 0 + a = a

-- Multiplication : propriétés fondamentales  
#check @Nat.mul_assoc    -- (a * b) * c = a * (b * c)
#check @Nat.mul_comm     -- a * b = b * a
#check @Nat.mul_one      -- a * 1 = a
#check @Nat.one_mul      -- 1 * a = a

-- Distributivite
#check @Nat.left_distrib  -- a * (b + c) = a * b + a * c
#check @Nat.right_distrib -- (a + b) * c = a * c + b * c

Lecture du catalogue algébrique — comment trouver son lemme

Le bloc de gauche énumère des théorèmes algébriques Mathlib (mul_comm, add_assoc, pow_succ, mul_distrib). Chaque nom suit la convention Namespace.Concept.property : Nat.add_comm est la commutativité de l’addition sur Nat, Monoid.mul_comm serait sur un monoïde général. Le nom EST la spécification — Lean 4 utilise cette convention pour la recherche (commande by exact? ou la recherche Moogle, section 5).

Stratégie de recherche : avant de prouver a + b = b + a manuellement, tenter add_comm ou laisser simp le trouver. La majorité des identités algébriques « évidentes » ont déjà un lemme Mathlib.
ring_nf et simp only [mul_comm] : normalisent une expression vers une forme canonique. simp applique un large registre de lemmes ; simp only [...] restreint aux lemmes nommés (plus contrôlé).
Pont : Lean-12 (sensibilité) utilise mul_comm, sum_add, et des lemmes de borne triangulaire (norm_sum). La fluidité avec le catalogue algébrique est un prérequis pour la partie haute.

4.3 Analyse

La cellule de gauche introduit l’analyse de Mathlib via import Mathlib.Analysis.Calculus.Deriv.Basic, le module qui définit HasDerivAt (la dérivée en un point comme limite du taux d’accroissement), les regles de derivation (deriv_add, deriv_mul au sens de Leibniz, deriv_pow), et l’ecosysteme des filtres pour les limites (Filter.Tendsto, tendsto_add, tendsto_mul). Sans ce module, Lean ignore tout de la continuite, des limites, de l’intégrale.

Pourquoi les filtres sont au coeur de l’analyse Mathlib

Unification : un seul mechanisme abstrait – tendsto f l₁ l₂ – capture limite en un point, limite a l’infini, continuite en un point, continuite globale, convergence de suites. Tous les théorèmes de passage a la limite ont la meme signature.
Puissance sans surprise : prouver lim (f + g) = lim f + lim g devient tendsto_add une seule fois, applicable partout ou la topologie le permet.
Pont direct avec Lean-12 (sensibilité de Huang) : ce notebook manipule la norme ‖·‖, prouve la borne ‖Σ x_i‖ ≤ Σ ‖x_i‖ (norme triangulaire), et utilise la continuite de la fonction norme. Tout repose sur Filter.Tendsto et Continuous sans jamais les nommer explicitement.

Dérivées comme limite – pas ε-δ manuel

La définition HasDerivAt f f' x est : il existe une fonctionnelle linéaire f' telle que (f (x + h) - f x - f' h) / ‖h‖ → 0 quand h → 0. Lean developpe ensuite les regles (hasDerivAt_add, hasDerivAt_pow, regle de la chaine) plutot que de demander a l’utilisateur de redeployer la définition ε-δ a chaque fois. C’est la meme logique que pour les groupes : on delegue a Mathlib la preuve des lemmes, on utilise les consequences.

Pont strategique vers les notebooks de la partie haute

Lean-12 (sensibilité), Lean-14 (Finiteness) et Lean-16b (Game of Life) s’appuient tous sur Mathlib.Analysis. Maîtriser la structure de Deriv.Basic est le seuil d’entrée : sans cela, les preuves avancees (norme ‖·‖, Finset.card, sensibilité ‖ε‖₂ = O(√n)) restent inaccessibles. Ce notebook est la porte d’entrée analytique – les suivants en sont les prolongements sectoriels.

/-!
## Analyse avec Mathlib

Avec `import Mathlib.Analysis.Calculus.Deriv.Basic`, on accede a :

**Dérivées :**
- `HasDerivAt` : Définition de la dérivée
- `deriv_add` : (f + g)' = f' + g'
- `deriv_mul` : (f * g)' = f' * g + f * g' (Leibniz)
- `deriv_pow` : (x^n)' = n * x^(n-1)

**Limites :**
- `Filter.Tendsto` : Définition des limites
- `tendsto_add` : lim(f + g) = lim f + lim g
- `tendsto_mul` : lim(f * g) = lim f * lim g

**Integration :**
- `MeasureTheory.integral_add` : Linearite de l'intégrale

L'analyse dans Mathlib utilise les filtres pour définir les limites
de maniere tres générale (limites en un point, a l'infini, etc.).
-/

-- L'analyse réelle necessite Mathlib
-- Voici un apercu des concepts disponibles dans Lean de base

-- Types numériques de base
#check Nat    -- Nombres naturels
#check Int    -- Entiers relatifs
#check Float  -- Flottants (approximation, pas pour preuves formelles)

-- Ordre sur les nombres
#check @Nat.le_trans     -- a <= b -> b <= c -> a <= c
#check @Nat.lt_of_le_of_lt  -- a <= b -> b < c -> a < c

-- Division euclidienne
#check @Nat.div_add_mod  -- n = n / d * d + n % d

/-!

## Analyse avec Mathlib

Avec `import Mathlib.Analysis.Calculus.Deriv.Basic`, on accede a :

**Dérivées :**

- `HasDerivAt` : Définition de la dérivée

- `deriv_add` : (f + g)' = f' + g'

- `deriv_mul` : (f * g)' = f' * g + f * g' (Leibniz)

- `deriv_pow` : (x^n)' = n * x^(n-1)

**Limites :**

- `Filter.Tendsto` : Définition des limites

- `tendsto_add` : lim(f + g) = lim f + lim g

- `tendsto_mul` : lim(f * g) = lim f * lim g

**Integration :**

- `MeasureTheory.integral_add` : Linearite de l'intégrale

L'analyse dans Mathlib utilise les filtres pour définir les limites

de maniere tres générale (limites en un point, a l'infini, etc.).

-/

-- L'analyse réelle necessite Mathlib

-- Voici un apercu des concepts disponibles dans Lean de base

-- Types numériques de base

#check Nat    -- Nombres naturels Nat : Type

#check Int    -- Entiers relatifs Int : Type

#check Float  -- Flottants (approximation, pas pour preuves formelles) Float : Type

-- Ordre sur les nombres

#check @Nat.le_trans     -- a <= b -> b <= c -> a <= c @Nat.le_trans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k

#check @Nat.lt_of_le_of_lt  -- a <= b -> b < c -> a < c @Nat.lt_of_le_of_lt : ∀ {n m k : Nat}, n ≤ m → m < k → n < k

-- Division euclidienne

#check @Nat.div_add_mod  -- n = n / d * d + n % d Nat.div_add_mod : ∀ (m n : Nat), n * (m / n) + m % n = m

--% env 11

Raw input

{"cmd": "/-!\n## Analyse avec Mathlib\n\nAvec `import Mathlib.Analysis.Calculus.Deriv.Basic`, on accede a :\n\n**D\u00e9riv\u00e9es :**\n- `HasDerivAt` : D\u00e9finition de la d\u00e9riv\u00e9e\n- `deriv_add` : (f + g)' = f' + g'\n- `deriv_mul` : (f * g)' = f' * g + f * g' (Leibniz)\n- `deriv_pow` : (x^n)' = n * x^(n-1)\n\n**Limites :**\n- `Filter.Tendsto` : D\u00e9finition des limites\n- `tendsto_add` : lim(f + g) = lim f + lim g\n- `tendsto_mul` : lim(f * g) = lim f * lim g\n\n**Integration :**\n- `MeasureTheory.integral_add` : Linearite de l'int\u00e9grale\n\nL'analyse dans Mathlib utilise les filtres pour d\u00e9finir les limites\nde maniere tres g\u00e9n\u00e9rale (limites en un point, a l'infini, etc.).\n-/\n\n-- L'analyse r\u00e9elle necessite Mathlib\n-- Voici un apercu des concepts disponibles dans Lean de base\n\n-- Types num\u00e9riques de base\n#check Nat    -- Nombres naturels\n#check Int    -- Entiers relatifs\n#check Float  -- Flottants (approximation, pas pour preuves formelles)\n\n-- Ordre sur les nombres\n#check @Nat.le_trans     -- a <= b -> b <= c -> a <= c\n#check @Nat.lt_of_le_of_lt  -- a <= b -> b < c -> a < c\n\n-- Division euclidienne\n#check @Nat.div_add_mod  -- n = n / d * d + n % d", "env": 10}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 28, "column": 0},
   "endPos": {"line": 28, "column": 6},
   "data": "Nat : Type"},
  {"severity": "info",
   "pos": {"line": 29, "column": 0},
   "endPos": {"line": 29, "column": 6},
   "data": "Int : Type"},
  {"severity": "info",
   "pos": {"line": 30, "column": 0},
   "endPos": {"line": 30, "column": 6},
   "data": "Float : Type"},
  {"severity": "info",
   "pos": {"line": 33, "column": 0},
   "endPos": {"line": 33, "column": 6},
   "data": "@Nat.le_trans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k"},
  {"severity": "info",
   "pos": {"line": 34, "column": 0},
   "endPos": {"line": 34, "column": 6},
   "data": "@Nat.lt_of_le_of_lt : ∀ {n m k : Nat}, n ≤ m → m < k → n < k"},
  {"severity": "info",
   "pos": {"line": 37, "column": 0},
   "endPos": {"line": 37, "column": 6},
   "data": "Nat.div_add_mod : ∀ (m n : Nat), n * (m / n) + m % n = m"}],
 "env": 11}

Lecture du catalogue analytique — limites, continuité, dérivées

Le bloc analytique (gauche) introduit les notions tendsto (limite), Continuous (continuité), HasDerivAt (dérivée). Mathlib encode l’analyse via des filtres (Filter) — un device unificateur pour limites, continuité, convergence topologique. tendsto f l₁ l₂ dit que f envoie le filtre l₁ vers l₂.

Pourquoi les filtres : ils unifient limite en un point, limite à l’infini, continuité, convergence de suites. Une fois le formalisme des filtres maîtrisé, tous les théorèmes de passage à la limite ont la même forme.
HasDerivAt f f' x vs la définition ε-δ : Mathlib définit la dérivée via la limite du taux d’accroissement, puis prouve les règles (somme, produit, chaîne). En pratique, on applique hasDerivAt_add, hasDerivAt_pow, etc.
Pont direct : Lean-14 (Finiteness) prouve la finitude des dérivées polynomiales — il utilise HasDerivAt, polynomial_deriv, et le catalogue analytique. Lean-12 (sensibilité) manipule la norme ‖·‖ et sa continuité. Cette section est le seuil d’entrée vers la partie haute : sans filtres ni HasDerivAt, les notebooks ≥12 sont inaccessibles.

5. Recherche et Navigation

5.1 Documentation en ligne

La documentation Mathlib est disponible sur : https://leanprover-community.github.io/mathlib4_docs/

5.2 Loogle : Recherche syntaxique

Loogle (https://loogle.lean-lang.org/) permet de chercher des théorèmes par leur signature de type.

/-!
## Loogle : Recherche syntaxique

**Loogle** (https://loogle.lean-lang.org/) permet de chercher des théorèmes 
par leur signature de type.

### Exemples de requetes Loogle :

| Requete | Recherche |
|---------|-----------|
| `?a + 0 = ?a` | Théorème sur addition et zero |
| `?a + ?b = ?b + ?a` | Commutativite de l'addition |
| `Nat.Prime, Nat.Odd` | Théorèmes impliquant Prime et Odd |

### Syntaxe :
- `?a` : Variable de type quelconque
- `_` : Argument dont on ne se soucie pas  
- `A -> B` : Fonction de A vers B
-/

-- Demonstration : chercher des théorèmes par leur forme
-- Ces théorèmes existent dans la bibliotheque standard de Lean

-- "?a + 0 = ?a" -> Nat.add_zero
#check @Nat.add_zero  -- forall n, n + 0 = n

-- "?a + ?b = ?b + ?a" -> Nat.add_comm
#check @Nat.add_comm  -- forall n m, n + m = m + n

-- "?a * 1 = ?a" -> Nat.mul_one
#check @Nat.mul_one   -- forall n, n * 1 = n

/-!

## Loogle : Recherche syntaxique

**Loogle** (https://loogle.lean-lang.org/) permet de chercher des théorèmes

par leur signature de type.

### Exemples de requetes Loogle :

| Requete | Recherche |

|---------|-----------|

| `?a + 0 = ?a` | Théorème sur addition et zero |

| `?a + ?b = ?b + ?a` | Commutativite de l'addition |

| `Nat.Prime, Nat.Odd` | Théorèmes impliquant Prime et Odd |

### Syntaxe :

- `?a` : Variable de type quelconque

- `_` : Argument dont on ne se soucie pas

- `A -> B` : Fonction de A vers B

-/

-- Demonstration : chercher des théorèmes par leur forme

-- Ces théorèmes existent dans la bibliotheque standard de Lean

-- "?a + 0 = ?a" -> Nat.add_zero

#check @Nat.add_zero  -- forall n, n + 0 = n Nat.add_zero : ∀ (n : Nat), n + 0 = n

-- "?a + ?b = ?b + ?a" -> Nat.add_comm

#check @Nat.add_comm  -- forall n m, n + m = m + n Nat.add_comm : ∀ (n m : Nat), n + m = m + n

-- "?a * 1 = ?a" -> Nat.mul_one

#check @Nat.mul_one   -- forall n, n * 1 = n Nat.mul_one : ∀ (n : Nat), n * 1 = n

--% env 12

Raw input

{"cmd": "/-!\n## Loogle : Recherche syntaxique\n\n**Loogle** (https://loogle.lean-lang.org/) permet de chercher des th\u00e9or\u00e8mes \npar leur signature de type.\n\n### Exemples de requetes Loogle :\n\n| Requete | Recherche |\n|---------|-----------|\n| `?a + 0 = ?a` | Th\u00e9or\u00e8me sur addition et zero |\n| `?a + ?b = ?b + ?a` | Commutativite de l'addition |\n| `Nat.Prime, Nat.Odd` | Th\u00e9or\u00e8mes impliquant Prime et Odd |\n\n### Syntaxe :\n- `?a` : Variable de type quelconque\n- `_` : Argument dont on ne se soucie pas  \n- `A -> B` : Fonction de A vers B\n-/\n\n-- Demonstration : chercher des th\u00e9or\u00e8mes par leur forme\n-- Ces th\u00e9or\u00e8mes existent dans la bibliotheque standard de Lean\n\n-- \"?a + 0 = ?a\" -> Nat.add_zero\n#check @Nat.add_zero  -- forall n, n + 0 = n\n\n-- \"?a + ?b = ?b + ?a\" -> Nat.add_comm\n#check @Nat.add_comm  -- forall n m, n + m = m + n\n\n-- \"?a * 1 = ?a\" -> Nat.mul_one\n#check @Nat.mul_one   -- forall n, n * 1 = n", "env": 11}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 25, "column": 0},
   "endPos": {"line": 25, "column": 6},
   "data": "Nat.add_zero : ∀ (n : Nat), n + 0 = n"},
  {"severity": "info",
   "pos": {"line": 28, "column": 0},
   "endPos": {"line": 28, "column": 6},
   "data": "Nat.add_comm : ∀ (n m : Nat), n + m = m + n"},
  {"severity": "info",
   "pos": {"line": 31, "column": 0},
   "endPos": {"line": 31, "column": 6},
   "data": "Nat.mul_one : ∀ (n : Nat), n * 1 = n"}],
 "env": 12}

5.3 Moogle : Recherche sémantique

Moogle (https://www.moogle.ai/) utilise des LLMs pour la recherche sémantique dans Mathlib - on peut chercher en langage naturel.

/-!
## Moogle : Recherche semantique

**Moogle** (https://www.moogle.ai/) utilise des LLMs pour la recherche 
semantique dans Mathlib - on peut chercher en langage naturel.

### Exemples de requetes Moogle :

| Requete (langage naturel) | Résultat |
|---------------------------|----------|
| "derivative of exponential function" | `Real.deriv_exp : deriv exp x = exp x` |
| "infinitely many prime numbers" | `Nat.exists_infinite_primes` |
| "triangle inequality" | `norm_add_le : ‖a + b‖ <= ‖a‖ + ‖b‖` |
| "fundamental theorem of calculus" | `intervalIntegral.integral_eq_sub_of_hasDerivAt` |

### Avantages de Moogle :
- Recherche en langage naturel
- Comprend les synonymes mathematiques
- Suggere des théorèmes connexes
-/

-- Demonstration de la recherche : lemmes utiles sur les listes
#check @List.length_append  -- length (l1 ++ l2) = length l1 + length l2
#check @List.length_reverse -- length (reverse l) = length l
#check @List.reverse_reverse -- reverse (reverse l) = l

/-!

## Moogle : Recherche semantique

**Moogle** (https://www.moogle.ai/) utilise des LLMs pour la recherche

semantique dans Mathlib - on peut chercher en langage naturel.

### Exemples de requetes Moogle :

| Requete (langage naturel) | Résultat |

|---------------------------|----------|

| "derivative of exponential function" | `Real.deriv_exp : deriv exp x = exp x` |

| "infinitely many prime numbers" | `Nat.exists_infinite_primes` |

| "triangle inequality" | `norm_add_le : ‖a + b‖ <= ‖a‖ + ‖b‖` |

| "fundamental theorem of calculus" | `intervalIntegral.integral_eq_sub_of_hasDerivAt` |

### Avantages de Moogle :

- Recherche en langage naturel

- Comprend les synonymes mathematiques

- Suggere des théorèmes connexes

-/

-- Demonstration de la recherche : lemmes utiles sur les listes

#check @List.length_append  -- length (l1 ++ l2) = length l1 + length l2 @List.length_append : ∀ {α : Type u_1} {as bs : List α}, (as ++ bs).length = as.length + bs.length

#check @List.length_reverse -- length (reverse l) = length l @List.length_reverse : ∀ {α : Type u_1} {as : List α}, as.reverse.length = as.length

#check @List.reverse_reverse -- reverse (reverse l) = l @List.reverse_reverse : ∀ {α : Type u_1} (as : List α), as.reverse.reverse = as

--% env 13

Raw input

{"cmd": "/-!\n## Moogle : Recherche semantique\n\n**Moogle** (https://www.moogle.ai/) utilise des LLMs pour la recherche \nsemantique dans Mathlib - on peut chercher en langage naturel.\n\n### Exemples de requetes Moogle :\n\n| Requete (langage naturel) | R\u00e9sultat |\n|---------------------------|----------|\n| \"derivative of exponential function\" | `Real.deriv_exp : deriv exp x = exp x` |\n| \"infinitely many prime numbers\" | `Nat.exists_infinite_primes` |\n| \"triangle inequality\" | `norm_add_le : \u2016a + b\u2016 <= \u2016a\u2016 + \u2016b\u2016` |\n| \"fundamental theorem of calculus\" | `intervalIntegral.integral_eq_sub_of_hasDerivAt` |\n\n### Avantages de Moogle :\n- Recherche en langage naturel\n- Comprend les synonymes mathematiques\n- Suggere des th\u00e9or\u00e8mes connexes\n-/\n\n-- Demonstration de la recherche : lemmes utiles sur les listes\n#check @List.length_append  -- length (l1 ++ l2) = length l1 + length l2\n#check @List.length_reverse -- length (reverse l) = length l\n#check @List.reverse_reverse -- reverse (reverse l) = l", "env": 12}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 23, "column": 0},
   "endPos": {"line": 23, "column": 6},
   "data":
   "@List.length_append : ∀ {α : Type u_1} {as bs : List α}, (as ++ bs).length = as.length + bs.length"},
  {"severity": "info",
   "pos": {"line": 24, "column": 0},
   "endPos": {"line": 24, "column": 6},
   "data":
   "@List.length_reverse : ∀ {α : Type u_1} {as : List α}, as.reverse.length = as.length"},
  {"severity": "info",
   "pos": {"line": 25, "column": 0},
   "endPos": {"line": 25, "column": 6},
   "data":
   "@List.reverse_reverse : ∀ {α : Type u_1} (as : List α), as.reverse.reverse = as"}],
 "env": 13}

5.4 Commandes de recherche dans Lean

/-!
## Commandes de recherche dans Lean

Lean (avec Mathlib) fournit des tactiques de recherche interactives :

| Commande | Usage |
|----------|-------|
| `exact?` | Cherche une preuve exacte dans le contexte et la bibliotheque |
| `apply?` | Cherche un lemme applicable au but courant |
| `rw?` | Suggere des reecritures possibles |
| `simp?` | Montre les regles simp utilisees |

### Exemples d'utilisation :

```lean
-- exact? cherche une preuve exacte
example (n : Nat) : n + 0 = n := by exact?
-- Résultat : exact Nat.add_zero n

-- apply? cherche un lemme a appliquer
example (n m : Nat) : n <= n + m := by apply?
-- Résultat : apply Nat.le_add_right

-- rw? suggere des reecritures
example (n : Nat) : 0 + n = n := by rw?
-- Résultat : rw [Nat.zero_add]
```
-/

-- Sans les tactiques de recherche Mathlib, on utilise les lemmes directement
-- Voici comment on applique ces lemmes manuellement

-- Au lieu de exact?, on utilise le lemme explicitement
example (n : Nat) : n + 0 = n := Nat.add_zero n

-- Au lieu de apply?, on connait le lemme a appliquer
example (n m : Nat) : n <= n + m := Nat.le_add_right n m

-- Au lieu de rw?, on specifie la reecriture
example (n : Nat) : 0 + n = n := by rw [Nat.zero_add]

/-!

## Commandes de recherche dans Lean

Lean (avec Mathlib) fournit des tactiques de recherche interactives :

| Commande | Usage |

|----------|-------|

| `exact?` | Cherche une preuve exacte dans le contexte et la bibliotheque |

| `apply?` | Cherche un lemme applicable au but courant |

| `rw?` | Suggere des reecritures possibles |

| `simp?` | Montre les regles simp utilisees |

### Exemples d'utilisation :

```lean

-- exact? cherche une preuve exacte

example (n : Nat) : n + 0 = n := by exact?

-- Résultat : exact Nat.add_zero n

-- apply? cherche un lemme a appliquer

example (n m : Nat) : n <= n + m := by apply?

-- Résultat : apply Nat.le_add_right

-- rw? suggere des reecritures

example (n : Nat) : 0 + n = n := by rw?

-- Résultat : rw [Nat.zero_add]

```

-/

-- Sans les tactiques de recherche Mathlib, on utilise les lemmes directement

-- Voici comment on applique ces lemmes manuellement

-- Au lieu de exact?, on utilise le lemme explicitement

example (n : Nat) : n + 0 = n := Nat.add_zero n

-- Au lieu de apply?, on connait le lemme a appliquer

example (n m : Nat) : n <= n + m := Nat.le_add_right n m

-- Au lieu de rw?, on specifie la reecriture

example (n : Nat) : 0 + n = n := by rw [Nat.zero_add]

--% env 14

Raw input

{"cmd": "/-!\n## Commandes de recherche dans Lean\n\nLean (avec Mathlib) fournit des tactiques de recherche interactives :\n\n| Commande | Usage |\n|----------|-------|\n| `exact?` | Cherche une preuve exacte dans le contexte et la bibliotheque |\n| `apply?` | Cherche un lemme applicable au but courant |\n| `rw?` | Suggere des reecritures possibles |\n| `simp?` | Montre les regles simp utilisees |\n\n### Exemples d'utilisation :\n\n```lean\n-- exact? cherche une preuve exacte\nexample (n : Nat) : n + 0 = n := by exact?\n-- R\u00e9sultat : exact Nat.add_zero n\n\n-- apply? cherche un lemme a appliquer\nexample (n m : Nat) : n <= n + m := by apply?\n-- R\u00e9sultat : apply Nat.le_add_right\n\n-- rw? suggere des reecritures\nexample (n : Nat) : 0 + n = n := by rw?\n-- R\u00e9sultat : rw [Nat.zero_add]\n```\n-/\n\n-- Sans les tactiques de recherche Mathlib, on utilise les lemmes directement\n-- Voici comment on applique ces lemmes manuellement\n\n-- Au lieu de exact?, on utilise le lemme explicitement\nexample (n : Nat) : n + 0 = n := Nat.add_zero n\n\n-- Au lieu de apply?, on connait le lemme a appliquer\nexample (n m : Nat) : n <= n + m := Nat.le_add_right n m\n\n-- Au lieu de rw?, on specifie la reecriture\nexample (n : Nat) : 0 + n = n := by rw [Nat.zero_add]", "env": 13}

Raw output

{"env": 14}

6. Cas d’Usage Avances

6.1 Terry Tao et la théorie analytique des nombres

En janvier 2026, Terence Tao (medaille Fields 2006) a utilise Mathlib4 pour formaliser des résultats en théorie analytique des nombres. Il a notamment contribue a :

Formalisation de lemmes sur les fonctions L de Dirichlet
Vérification de bornes asymptotiques pour la fonction pi(x)
Travail vers une preuve formelle complète du théorème des nombres premiers

Cet événement marque un tournant : un mathematicien de premier plan utilise la vérification formelle comme outil de recherche quotidien.

6.2 Théorèmes majeurs formalises dans Mathlib

Théorème	Domaine	Auteur original
Dernier théorème de Fermat	Théorie des nombres	Fermat/Wiles
Théorème des nombres premiers	Analyse	Hadamard/de la Vallee Poussin
Théorème de Bolzano-Weierstrass	Analyse	Bolzano
Lemme de Zorn	Théorie des ensembles	Zorn
Théorème de Hahn-Banach	Analyse fonctionnelle	Hahn/Banach
Théorème de Stone-Weierstrass	Approximation	Stone/Weierstrass

6.3 Lean4Lean : Le bootstrap (POPL 2026)

Lean4Lean est un projet ambitieux qui vise a reimplementer Lean 4 en Lean 4 lui-même. Presente a POPL 2026, il démontre :

Auto-hebergement : Lean peut se compiler lui-même
Vérification : Le compilateur est prouvé correct
Confiance accrue : Reduit la base de code “de confiance”

6.4 Impact sur la recherche mathematique

Avant la formalisation : - Revue par pairs humaine, erreurs possibles - Temps de vérification : mois/annees - Confiance : depend de la reputation

Avec Mathlib/Lean : - Vérification automatique, certitude mathematique - Temps : minutes/heures pour vérifier - Confiance : absolue si la preuve compile

7. Exercices — corriges

Corriges issus du rendu étudiant (PR #2563), valides a l’exécution. Les exercices a completer restent en fin de notebook.

Exercice 1 : Utiliser omega

-- Prouver avec omega
theorem ex1 (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by
  omega

-- Prouver avec omega

theorem ex1 (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by

  omega

--% env 15

Raw input

{"cmd": "-- Prouver avec omega\ntheorem ex1 (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by\n  omega", "env": 14}

Raw output

{"env": 15}

Exercice 2 : Calculer avec rfl/decide

-- Prouver ces calculs
theorem ex2a : 7 * 8 = 56 := by rfl
theorem ex2b : 100 > 50 := by decide

-- Prouver ces calculs

theorem ex2a : 7 * 8 = 56 := by rfl

theorem ex2b : 100 > 50 := by decide

--% env 16

Raw input

{"cmd": "-- Prouver ces calculs\ntheorem ex2a : 7 * 8 = 56 := by rfl\ntheorem ex2b : 100 > 50 := by decide", "env": 15}

Raw output

{"env": 16}

Exercice 3 : Preuve manuelle style Mathlib

-- Prouver l'associativite de l'addition sur Nat
-- (sans utiliser directement Nat.add_assoc)
theorem ex3 (a b c : Nat) : (a + b) + c = a + (b + c) := by
  omega

-- Prouver l'associativite de l'addition sur Nat

-- (sans utiliser directement Nat.add_assoc)

theorem ex3 (a b c : Nat) : (a + b) + c = a + (b + c) := by

  omega

--% env 17

Raw input

{"cmd": "-- Prouver l'associativite de l'addition sur Nat\n-- (sans utiliser directement Nat.add_assoc)\ntheorem ex3 (a b c : Nat) : (a + b) + c = a + (b + c) := by\n  omega", "env": 16}

Raw output

{"env": 17}

Exercices a completer

-- Exercice 1 : Preuve arithmetique avec omega
-- TODO étudiant : prouver a < 10 a partir de a + b = c et c < 10
-- Indice : omega resout automatiquement l'arithmetique de Presburger
theorem ex1_practice (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by
  sorry

-- Exercice 1 : Preuve arithmetique avec omega

-- TODO étudiant : prouver a < 10 a partir de a + b = c et c < 10

-- Indice : omega resout automatiquement l'arithmetique de Presburger

theorem ex1_practice (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by🟨 declaration uses `sorry`

  sorry

--% env 18

--% prove 0

Raw input

{"cmd": "-- Exercice 1 : Preuve arithmetique avec omega\n-- TODO \u00e9tudiant : prouver a < 10 a partir de a + b = c et c < 10\n-- Indice : omega resout automatiquement l'arithmetique de Presburger\ntheorem ex1_practice (a b c : Nat) (h1 : a + b = c) (h2 : c < 10) : a < 10 := by\n  sorry", "env": 17}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 5, "column": 2},
   "goal": "a b c : Nat\nh1 : a + b = c\nh2 : c < 10\n⊢ a < 10",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 8},
   "endPos": {"line": 4, "column": 20},
   "data": "declaration uses `sorry`"}],
 "env": 18}

Exercice 1 : Calculer avec `rfl` et `decide`

Prouvez ces assertions numériques simples. Pensez a utiliser rfl pour les égalités definitionnelles et decide pour les propositions decidables.

-- Exercice 2 : Preuves simples avec rfl et decide
-- TODO étudiant : prouver 7 * 8 = 56 et 100 > 50
-- Indice : rfl pour les égalités, decide pour les comparaisons
theorem ex2a_practice : 7 * 8 = 56 := by sorry
theorem ex2b_practice : 100 > 50 := by sorry

-- Exercice 2 : Preuves simples avec rfl et decide

-- TODO étudiant : prouver 7 * 8 = 56 et 100 > 50

-- Indice : rfl pour les égalités, decide pour les comparaisons

theorem ex2a_practice : 7 * 8 = 56 := by sorry🟨 declaration uses `sorry`

theorem ex2b_practice : 100 > 50 := by sorry🟨 declaration uses `sorry`

--% env 19

--% prove 2

Raw input

{"cmd": "-- Exercice 2 : Preuves simples avec rfl et decide\n-- TODO \u00e9tudiant : prouver 7 * 8 = 56 et 100 > 50\n-- Indice : rfl pour les \u00e9galit\u00e9s, decide pour les comparaisons\ntheorem ex2a_practice : 7 * 8 = 56 := by sorry\ntheorem ex2b_practice : 100 > 50 := by sorry", "env": 18}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 4, "column": 41},
   "goal": "⊢ 7 * 8 = 56",
   "endPos": {"line": 4, "column": 46}},
  {"proofState": 2,
   "pos": {"line": 5, "column": 39},
   "goal": "⊢ 100 > 50",
   "endPos": {"line": 5, "column": 44}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 8},
   "endPos": {"line": 4, "column": 21},
   "data": "declaration uses `sorry`"},
  {"severity": "warning",
   "pos": {"line": 5, "column": 8},
   "endPos": {"line": 5, "column": 21},
   "data": "declaration uses `sorry`"}],
 "env": 19}

Exercice 2 : Associativite avec `omega`

Prouvez l’associativite de l’addition sur Nat. La tactique omega resout directement les égalités arithmetiques sur les naturels.

-- Exercice 3 : Associativite de l'addition
-- TODO étudiant : utiliser omega ou le lemme Nat.add_assoc
-- Indice : omega resout cette égalité directement
theorem ex3_practice (a b c : Nat) : (a + b) + c = a + (b + c) := by
  sorry

-- Exercice 3 : Associativite de l'addition

-- TODO étudiant : utiliser omega ou le lemme Nat.add_assoc

-- Indice : omega resout cette égalité directement

theorem ex3_practice (a b c : Nat) : (a + b) + c = a + (b + c) := by🟨 declaration uses `sorry`

  sorry

--% env 20

--% prove 3

Raw input

{"cmd": "-- Exercice 3 : Associativite de l'addition\n-- TODO \u00e9tudiant : utiliser omega ou le lemme Nat.add_assoc\n-- Indice : omega resout cette \u00e9galit\u00e9 directement\ntheorem ex3_practice (a b c : Nat) : (a + b) + c = a + (b + c) := by\n  sorry", "env": 19}

Raw output

{"sorries":
 [{"proofState": 3,
   "pos": {"line": 5, "column": 2},
   "goal": "a b c : Nat\n⊢ a + b + c = a + (b + c)",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 8},
   "endPos": {"line": 4, "column": 20},
   "data": "declaration uses `sorry`"}],
 "env": 20}

Exercice 3 : Simplification avec `simp`

La tactique simp reecrit automatiquement en utilisant des lemmes marques @[simp]. Utilisez-la pour prouver que doubler un naturel et diviser par 2 redonne le même nombre.

-- Exercice 4 : Simplification automatique avec simp
-- TODO étudiant : prouver que n * 2 / 2 = n
-- Indice : simp [Nat.mul_comm, Nat.div_mul] peut aider, ou omega
theorem ex4_practice (n : Nat) : n * 2 / 2 = n := by
  sorry

-- Exercice 4 : Simplification automatique avec simp

-- TODO étudiant : prouver que n * 2 / 2 = n

-- Indice : simp [Nat.mul_comm, Nat.div_mul] peut aider, ou omega

theorem ex4_practice (n : Nat) : n * 2 / 2 = n := by🟨 declaration uses `sorry`

  sorry

--% env 21

--% prove 4

Raw input

{"cmd": "-- Exercice 4 : Simplification automatique avec simp\n-- TODO \u00e9tudiant : prouver que n * 2 / 2 = n\n-- Indice : simp [Nat.mul_comm, Nat.div_mul] peut aider, ou omega\ntheorem ex4_practice (n : Nat) : n * 2 / 2 = n := by\n  sorry", "env": 20}

Raw output

{"sorries":
 [{"proofState": 4,
   "pos": {"line": 5, "column": 2},
   "goal": "n : Nat\n⊢ n * 2 / 2 = n",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 8},
   "endPos": {"line": 4, "column": 20},
   "data": "declaration uses `sorry`"}],
 "env": 21}

Exercice 4 : Système d’équations avec `omega`

omega peut aussi resoudre des systèmes d’équations linéaires. Prouvez la valeur de a a partir de deux équations.

-- Exercice 5 : Resolution de système linéaire
-- TODO étudiant : a partir de a + b = 10 et a - b = 4, prouver a = 7
-- Indice : omega resout les systemes linéaires sur Nat/Int
theorem ex5_practice (a b : Nat) (h1 : a + b = 10) (h2 : a - b = 4) : a = 7 := by
  sorry

-- Exercice 5 : Resolution de système linéaire

-- TODO étudiant : a partir de a + b = 10 et a - b = 4, prouver a = 7

-- Indice : omega resout les systemes linéaires sur Nat/Int

theorem ex5_practice (a b : Nat) (h1 : a + b = 10) (h2 : a - b = 4) : a = 7 := by🟨 declaration uses `sorry`

  sorry

--% env 22

--% prove 5

Raw input

{"cmd": "-- Exercice 5 : Resolution de syst\u00e8me lin\u00e9aire\n-- TODO \u00e9tudiant : a partir de a + b = 10 et a - b = 4, prouver a = 7\n-- Indice : omega resout les systemes lin\u00e9aires sur Nat/Int\ntheorem ex5_practice (a b : Nat) (h1 : a + b = 10) (h2 : a - b = 4) : a = 7 := by\n  sorry", "env": 21}

Raw output

{"sorries":
 [{"proofState": 5,
   "pos": {"line": 5, "column": 2},
   "goal": "a b : Nat\nh1 : a + b = 10\nh2 : a - b = 4\n⊢ a = 7",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 8},
   "endPos": {"line": 4, "column": 20},
   "data": "declaration uses `sorry`"}],
 "env": 22}

Resume

Tactiques Mathlib essentielles

Tactique	Domaine	Usage	Disponibilite
`ring`	Algebre	Égalités polynomiales	Mathlib
`linarith`	Arithmetique	Inégalités linéaires	Mathlib
`omega`	Presburger	Arithmetique avec +, -, <	Lean de base
`norm_num`	Calcul	Expressions numériques	Mathlib
`field_simp`	Corps	Fractions et divisions	Mathlib
`polyrith`	Polynomes	Certificats via Sage	Mathlib
`simp`	Général	Simplification automatique	Lean de base
`exact?`	Recherche	Trouver une preuve exacte	Mathlib
`apply?`	Recherche	Trouver un lemme applicable	Mathlib
`decide`	Decision	Propositions decidables	Lean de base
`rfl`	Égalité	Reflexivite definitionnelle	Lean de base

Structure Mathlib4

Namespace	Contenu principal
`Mathlib.Data`	List, Set, Finset, Multiset, Nat, Int, Rat
`Mathlib.Algebra`	Group, Ring, Field, Module, LinearMap
`Mathlib.Order`	Lattice, Order, Filter
`Mathlib.Topology`	TopologicalSpace, Compactness, Continuity
`Mathlib.Analysis`	Limits, Derivatives, Integrals, Measures
`Mathlib.NumberTheory`	Prime, Divisibility, Modular arithmetic
`Mathlib.Tactic`	ring, linarith, omega, norm_num, etc.

Ressources

Ressource	URL	Usage
Documentation officielle	https://leanprover-community.github.io/mathlib4_docs/	Reference complète
Loogle	https://loogle.lean-lang.org/	Recherche par signature de type
Moogle	https://www.moogle.ai/	Recherche en langage naturel
Repository GitHub	https://github.com/leanprover-community/mathlib4	Code source
Zulip Chat	https://leanprover.zulipchat.com/	Communaute et support
Mathematics in Lean	https://leanprover-community.github.io/mathematics_in_lean/	Tutoriel approfondi

Commandes de recherche

-- exact? : trouve une preuve exacte
-- apply? : trouve un lemme a appliquer  
-- rw?    : suggere des reecritures
-- simp?  : montre les règles simp utilisees

Prochaine étape

Dans le notebook Lean-07-LLM-Integration-Lean-Python, nous verrons comment les Large Language Models peuvent assister la construction de preuves Lean, avec des outils comme LeanCopilot (NeurIPS 2025), LeanProgress (TMLR 2025), et les percees recentes d’AlphaProof (Nature 2025).

Notebook base sur l’état de l’art Mathlib4 v4.27.0-rc1 (janvier 2026) Ressources : leanprover-community.github.io, Terry Tao blog, Lean4Lean (POPL 2026)

Navigation : ← Lean-05-Tactics-Lean | Index | Lean-07-LLM-Integration-Lean-Python →

Lire un théorème Mathlib : le nom EST la spécification

Avec Mathlib, le nom du théorème porte l’information mathématique — c’est la convention Namespace.Concept.property. Cette grille de lecture évite de se perdre dans la jungle des ~100 000 lemmes.

Décodage systématique d’un nom (cf. cellules 32 « Lecture du catalogue algébrique » et 35 « Lecture du catalogue analytique ») :

Segment 1 (avant le premier .) : le namespace indique où vit le théorème.
- Nat.add_comm → vit dans Nat, le namespace des entiers naturels.
- Monoid.mul_comm → vit dans Monoid, le namespace des structures de monoïde (plus général que Nat).
- Continuous.continuous_add → vit dans Continuous (préfixe de lemme attaché à la structure Continuous).
Segments suivants : la spécification, lue comme une phrase anglaise.
- add_comm = addition is commutative.
- mul_assoc = multiplication is associative.
- hasDerivAt_add = the derivative of a sum is the sum of derivatives.
- tendsto_id = the identity function tends to itself (trivial mais explicite).
Préfixes has_, Is_, Set_ : indiquent un typeclass ou une qualification.
- hasDerivAt f f' x se lit « f has derivative f' at x ».
- IsLimit s l se lit « s is a sequence with limit l ».

Application : face à Continuous.comp, on lit immédiatement « the composition of continuous functions is continuous » — pas besoin d’ouvrir le source pour deviner. C’est l’inverse du « terme-caché-qu’on-doit-déchiffrer » qu’on trouve dans certaines libs.

Stratégie de recherche :

Lire le nom : identifier le namespace + la propriété attendue.
Tenter apply? / exact? : Lean propose automatiquement le lemme dont la signature correspond au but.
Tenter rw? / simp? : pour les étapes de réécriture / simplification.
Si rien ne marche, chercher par nom dans Moogle (recherche sémantique en langage naturel) ou Loogle (recherche par signature de type). Cf. cellules 38 et 40.

Réflexe à transmettre : avant de prouver manuellement une identité « évidente » (a + b = b + a, 0 + n = n, ‖x + y‖ ≤ ‖x‖ + ‖y‖), toujours tester si Mathlib n’a pas déjà le lemme. La majorité des preuves « from scratch » dans la partie haute (Lean-12+) réutilisent ~80 % de lemmes Mathlib, et ne font que la glue — exactement l’insight « state preconditions precisely; compose existing guarantees » de la grille de lecture Lean-3/4.

Pour aller plus loin — Surviving proofs, The Importance of Understanding (05/09/2026) Sheydvasser, à l’article 1, recommande en principe 2 de situer un énoncé dans son réseau de concepts. La convention Mathlib Namespace.Concept.property qu’on présente ici (Semiring → Ring → CommRing → Field) est précisément la réalisation systématique de ce geste : un théorème n’est jamais isolé, il porte dans son nom les liens de généralisation et de spécialisation qui le rendent lisible. Le fait que Nat.exists_infinite_primes puisse se reformuler comme Nat.Infinite : Set ℕ puis comme Nat.exists_infinite_primes est exactement la généralisation qu’elle défend à l’article 1. Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/the-importance-of-understanding Archivé : G:DriveIA-Proves-Surviving-Proofs\2026-09-05_the-importance-of-understanding.html

Retour au sommet

Introduction

Pourquoi Mathlib est revolutionnaire

Objectifs pedagogiques

Prerequis

Duree estimee : 45-50 minutes

Contexte : L’Ecosysteme Mathlib

Historique

État actuel (Janvier 2026)

1. Installation et Configuration

1.1 Créer un projet avec Mathlib

1.1 Créer un projet avec Mathlib (Terminal)

1.2 lakefile.lean type pour Mathlib

1.3 Importer Mathlib

Pourquoi ces imports ouvrent toute la bibliothèque

2. Structure de Mathlib4

2.1 Organisation des modules

2.2 Hiérarchie de structures algébriques

Hiérarchie des typeclasses — l’algèbre en couches

3. Tactiques Mathlib Essentielles

3.1 ring : Algebre polynomiale

ring — la tactique de l’anneau commutatif

3.2 linarith : Arithmetique linéaire

Pourquoi linarith existe (et quand l’utiliser)

linarith — l’arithmétique linéaire réelle

3.3 omega : Arithmetique Presburger

omega — l’arithmétique de Presburger

3.4 norm_num : Calcul numérique

norm_num — le calcul numérique exact

3.5 field_simp : Simplification dans les corps

Pourquoi field_simp est necessaire (les simp classiques echouent)

3.6 polyrith : Certificats polynomiaux

Pourquoi polyrith complète omega et ring

4. Exemples de Théorèmes Mathlib

4.1 Théorie des nombres

4.2 Algebre

Pourquoi Group.Basic est le bon point d’entrée

Strategie de lecture du bloc code

Lecture du catalogue algébrique — comment trouver son lemme

4.3 Analyse

Pourquoi les filtres sont au coeur de l’analyse Mathlib

Dérivées comme limite – pas ε-δ manuel

Pont strategique vers les notebooks de la partie haute

Lecture du catalogue analytique — limites, continuité, dérivées

5. Recherche et Navigation

5.1 Documentation en ligne

5.2 Loogle : Recherche syntaxique

5.3 Moogle : Recherche sémantique

5.4 Commandes de recherche dans Lean

6. Cas d’Usage Avances

6.1 Terry Tao et la théorie analytique des nombres

6.2 Théorèmes majeurs formalises dans Mathlib

6.3 Lean4Lean : Le bootstrap (POPL 2026)

6.4 Impact sur la recherche mathematique

7. Exercices — corriges

Exercice 1 : Utiliser omega

Exercice 2 : Calculer avec rfl/decide

Exercice 3 : Preuve manuelle style Mathlib

Exercices a completer

Exercice 1 : Calculer avec rfl et decide

Exercice 2 : Associativite avec omega

Exercice 3 : Simplification avec simp

Exercice 4 : Système d’équations avec omega

Resume

Tactiques Mathlib essentielles

Structure Mathlib4

Ressources

Commandes de recherche

Prochaine étape

Lire un théorème Mathlib : le nom EST la spécification

3.1 `ring` : Algebre polynomiale

`ring` — la tactique de l’anneau commutatif

3.2 `linarith` : Arithmetique linéaire

Pourquoi `linarith` existe (et quand l’utiliser)

`linarith` — l’arithmétique linéaire réelle

3.3 `omega` : Arithmetique Presburger

`omega` — l’arithmétique de Presburger

3.4 `norm_num` : Calcul numérique

`norm_num` — le calcul numérique exact

3.5 `field_simp` : Simplification dans les corps

Pourquoi `field_simp` est necessaire (les `simp` classiques echouent)

3.6 `polyrith` : Certificats polynomiaux

Pourquoi `polyrith` complète `omega` et `ring`

Pourquoi `Group.Basic` est le bon point d’entrée

Exercice 1 : Calculer avec `rfl` et `decide`

Exercice 2 : Associativite avec `omega`

Exercice 3 : Simplification avec `simp`

Exercice 4 : Système d’équations avec `omega`