Lean-24b : Confiance et preuves — quand un certificat formel trompe

Navigation : Index | << Précédent | Série Lean

Un théorème Lean est un certificat : le kernel n’a laissé passer que ce qui est prouvé. Mais la confiance ne se résume pas à « le kernel a dit oui » : elle dépend aussi de ce qui a été prouvé, et avec quels axiomes. Ce notebook rend mesurables trois modes de « slop » formel identifiés par Dougherty et von Hippel (2026) dans Lies, Damned Lies, and Proofs — Formal Methods are not Slopless : la mis-définition (une définition si large que la preuve devient trivialement vraie), les axiomes de secours (sorry, native_decide, choix classique) et l’écart certificat / headline (l’énoncé formalisé ne dit pas la phrase qui sera vulgarisée). La source est archivée au gisement partagé du cluster (une copie unique, hors dépôt) ; les pages citées sont celles du PDF.

Objectifs, prérequis et durée

À la fin de ce parcours, vous saurez :

construire une preuve trivialement vraie par mis-définition et la reconnaître, même quand #print axioms est vide ;
lire #print axioms comme l’instrument de la confiance — le trio attendu [propext, Classical.choice, Quot.sound] ;
distinguer les deux axiomes de secours sorryAx et la réduction native (native_decide), et expliquer pourquoi une contradiction (False) implose toute la théorie ;
expliquer pourquoi les axiomes ne mesurent pas la fidélité de l’énoncé — les deux axes sont orthogonaux ;
appliquer la liste de confiance en trois questions avant de vulgariser un théorème.

Prérequis. Une installation Lean 4 fonctionnelle (kernel lean4-wsl), et les tactiques élémentaires rfl, trivial, norm_num, exact. La lecture des sorties #print axioms est le fil rouge de la série (cf. Lean-15c).

Durée. ~20 minutes.

1. Mis-définition : la preuve trivialement vraie (p. 4)

La source (p. 4) : « it’s very common that you mis-define some concept such that the proof is accidentally trivial ». Le kernel vérifie la preuve, pas la définition : si un prédicat est défini assez large, tout énoncé qui s’en sert devient une trivialité — et le certificat est valide sans être informative. Aucun organe automatique ne le détecte ; la lecture de la définition est un geste humain.

import Mathlib.Tactic
import Mathlib.Data.Nat.Basic

namespace Lean35Confiance

-- Premiere definition, trop large : « b divise a » est vrai pour tout couple.
-- Les binders muets _b _a taisent le linter ; la lecon reste : la definition ignore ses arguments.
def DivPar (_b _a : Nat) : Prop := True

theorem deuxDiviseTroisVide : DivPar 3 2 := by trivial
theorem zeroDiviseToutVide : DivPar 1 0 := by trivial

#print axioms deuxDiviseTroisVide
#print axioms zeroDiviseToutVide

import Mathlib.Tactic

import Mathlib.Data.Nat.Basic

namespace Lean35Confiance

-- Premiere definition, trop large : « b divise a » est vrai pour tout couple.

-- Les binders muets _b _a taisent le linter ; la lecon reste : la definition ignore ses arguments.

def DivPar (_b _a : Nat) : Prop := True

theorem deuxDiviseTroisVide : DivPar 3 2 := by trivial

theorem zeroDiviseToutVide : DivPar 1 0 := by trivial

#print axioms deuxDiviseTroisVide 'Lean35Confiance.deuxDiviseTroisVide' does not depend on any axioms

#print axioms zeroDiviseToutVide 'Lean35Confiance.zeroDiviseToutVide' does not depend on any axioms

--% env 0

Raw input

{"cmd": "import Mathlib.Tactic\nimport Mathlib.Data.Nat.Basic\n\nnamespace Lean35Confiance\n\n-- Premiere definition, trop large : \u00ab b divise a \u00bb est vrai pour tout couple.\n-- Les binders muets _b _a taisent le linter ; la lecon reste : la definition ignore ses arguments.\ndef DivPar (_b _a : Nat) : Prop := True\n\ntheorem deuxDiviseTroisVide : DivPar 3 2 := by trivial\ntheorem zeroDiviseToutVide : DivPar 1 0 := by trivial\n\n#print axioms deuxDiviseTroisVide\n#print axioms zeroDiviseToutVide\n"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data":
   "'Lean35Confiance.deuxDiviseTroisVide' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data":
   "'Lean35Confiance.zeroDiviseToutVide' does not depend on any axioms"}],
 "env": 0}

Lecture du résultat

Les deux théorèmes passent avec trivial, et #print axioms ne cite aucun axiome. C’est un certificat parfaitement valide — et entièrement creux : « 3 divise 2 » et « 1 divise 0 » sont prouvés sans le moindre calcul, parce que la définition ne porte pas la divisibilité. C’est le mode 1 du slop formel : énoncé vrai, preuve valide, valeur nulle. La preuve est vide au sens du contenu : il n’y a rien à lire dans le terme.

-- Raffinement : la definition porte vraiment la relation b | a.
def DivParVraie (b a : Nat) : Prop := b ≠ 0 ∧ ∃ k : Nat, a = b * k

theorem huitSurQuatre : DivParVraie 4 8 := ⟨by norm_num, ⟨2, by norm_num⟩⟩

#print axioms huitSurQuatre

-- Et la meme relation n'est plus prouvable a la volee : 2 ne divise pas 3.
example : ¬ DivParVraie 2 3 := by
  rintro ⟨hnz, ⟨k, hk⟩⟩
  omega

-- Raffinement : la definition porte vraiment la relation b | a.

def DivParVraie (b a : Nat) : Prop := b ≠ 0 ∧ ∃ k : Nat, a = b * k

theorem huitSurQuatre : DivParVraie 4 8 := ⟨by norm_num, ⟨2, by norm_num⟩⟩

#print axioms huitSurQuatre 'Lean35Confiance.huitSurQuatre' depends on axioms: [propext]

-- Et la meme relation n'est plus prouvable a la volee : 2 ne divise pas 3.

example : ¬ DivParVraie 2 3 := by

  rintro ⟨hnz, ⟨k, hk⟩⟩

  omega

--% env 1

Raw input

{"cmd": "-- Raffinement : la definition porte vraiment la relation b | a.\ndef DivParVraie (b a : Nat) : Prop := b \u2260 0 \u2227 \u2203 k : Nat, a = b * k\n\ntheorem huitSurQuatre : DivParVraie 4 8 := \u27e8by norm_num, \u27e82, by norm_num\u27e9\u27e9\n\n#print axioms huitSurQuatre\n\n-- Et la meme relation n'est plus prouvable a la volee : 2 ne divise pas 3.\nexample : \u00ac DivParVraie 2 3 := by\n  rintro \u27e8hnz, \u27e8k, hk\u27e9\u27e9\n  omega\n", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data": "'Lean35Confiance.huitSurQuatre' depends on axioms: [propext]"}],
 "env": 1}

Lecture du résultat

Le certificat ne porte aucun axiome de secours — [propext] seulement, la routine de norm_num — mais le terme porte maintenant un témoin : dans <by norm_num, ⟨2, by norm_num⟩>, le 2 est la preuve que 8 = 4 * 2. Le deuxième example montre le vrai coût : 2 ne divise pas 3, et c’est omega — pas trivial — qui le prouve, après que rintro a ouvert la conjonction et l’existentiel. Retenez la leçon : un certificat sans axiome de secours n’est pas une preuve substantielle. Les axiomes et la vacuité se mesurent sur deux axes distincts.

2. Axiomes de secours : les « proofs of false » (p. 6)

La source (p. 6) appelle « proofs of false » les certificats bâtis sur du sable : un axiome de secours peut rendre prouvable n’importe quoi, y compris False. Trois classes de secours, et l’organe qui les nomme : #print axioms.

2.1 `sorry` : l’axiome de secours transitif

Un sorry laissé dans une preuve n’est pas une erreur de syntaxe : la déclaration passe, et le kernel la marque d’un axiome dédié. Le danger n’est pas le sorry visible — c’est le sorry transitif, hérité d’un lemme apparemment propre mais prouvé avec un trou plus loin.

theorem fauxParTrou : False := by sorry

#print axioms fauxParTrou

theorem fauxParTrou : False := by sorry🟨 declaration uses `sorry`

#print axioms fauxParTrou 'Lean35Confiance.fauxParTrou' depends on axioms: [sorryAx]

--% env 2

--% prove 0

Raw input

{"cmd": "theorem fauxParTrou : False := by sorry\n\n#print axioms fauxParTrou\n", "env": 1}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 34},
   "goal": "⊢ False",
   "endPos": {"line": 1, "column": 39}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 19},
   "data": "declaration uses `sorry`"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data": "'Lean35Confiance.fauxParTrou' depends on axioms: [sorryAx]"}],
 "env": 2}

Lecture du résultat

Le #print axioms répond sorryAx : un axiome qui n’est ni dans Mathlib ni dans la théorie du kernel. Dès qu’il existe, False est prouvé — et avec False, tout le reste suit (section 2.4). Un grep sorry naïf sur les fichiers du dépôt ne voit que les occurrences littérales ; sorryAx est transitif : un lemme propre dont la preuve appelle un lemme prouvé par sorry porte l’axiome sans qu’aucun sorry n’apparaisse à sa ligne. C’est pour cela que le dépôt compte les sorry réels via scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry), jamais par grep.

2.2 `native_decide` : la réduction native sans preuve

native_decide ne construit pas une preuve par les règles : il demande à l’exécuteur natif de calculer si la proposition est vraie, puis demande au kernel de faire confiance à la réduction. Selon la taille du calcul, le kernel ne re-vérifie pas la réduction complète et l’axiome de secours apparaît — si le calcul est assez petit, il s’en sort sans axiome. #print axioms tranche.

#eval decide ((2 : Nat) ^ 200 ≤ 3 ^ 200)

theorem grandVrai : (2 : Nat) ^ 200 ≤ 3 ^ 200 := by native_decide

#print axioms grandVrai

#eval decide ((2 : Nat) ^ 200 ≤ 3 ^ 200) true

theorem grandVrai : (2 : Nat) ^ 200 ≤ 3 ^ 200 := by native_decide

#print axioms grandVrai 'Lean35Confiance.grandVrai' depends on axioms: [propext, grandVrai._native.native_decide.ax_1]

--% env 3

Raw input

{"cmd": "#eval decide ((2 : Nat) ^ 200 \u2264 3 ^ 200)\n\ntheorem grandVrai : (2 : Nat) ^ 200 \u2264 3 ^ 200 := by native_decide\n\n#print axioms grandVrai\n", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "'Lean35Confiance.grandVrai' depends on axioms: [propext, grandVrai._native.native_decide.ax_1]"}],
 "env": 3}

Lecture du résultat

Sur ce calculateur, #print axioms répond [propext, grandVrai._native.native_decide.ax_1] : le calcul 2 ^ 200 ≤ 3 ^ 200 est trop gros pour que le kernel re-vérifie la réduction, et le certificat repose sur la parole de l’exécuteur natif — une preuve par délégation. Le nom exact de l’axiome (native_decide.ax_1, porté par la déclaration grandVrai) varie avec la version du noyau et la taille du calcul : un calcul assez petit passe sans axiome. La leçon : il faut le mesurer, jamais le supposer. Les instruments du dépôt (le vérificateur proof-integrity du workflow Lean) traitent native_decide.* comme une classe d’axiomes à interdire par défaut, sauf justification écrite et nommée.

2.3 Le choix classique : légitime, mais nommé

Le tiers de loi classique n’est pas prouvable par les règles constructives : il repose sur Classical.choice, l’axiome du choix. C’est un axiome légitime et omniprésent dans Mathlib — le trio normal [propext, Classical.choice, Quot.sound] l’inclut. Le danger n’est pas sa présence : c’est qu’il soit masqué dans un axiome de secours, ou ajouté sans nécessité là où une preuve constructive eût suffi.

theorem ouClassique (P : Prop) : P ∨ ¬ P := Classical.em P

#print axioms ouClassique

theorem ouClassique (P : Prop) : P ∨ ¬ P := Classical.em P

#print axioms ouClassique 'Lean35Confiance.ouClassique' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 4

Raw input

{"cmd": "theorem ouClassique (P : Prop) : P \u2228 \u00ac P := Classical.em P\n\n#print axioms ouClassique\n", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "'Lean35Confiance.ouClassique' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 4}

Lecture du résultat

#print axioms ouClassique ne cite que Classical.choice : le tiers exclu en sort par dérivation. Sur le dépôt, la politique n’est pas « zéro Classical.choice » (Mathlib sans lui est inutilisable) : c’est une whiteliste par nom explicite, jamais par wildcard — tout nouvel axiome non listé fait rougir le garde.

2.4 Implosion : une fois `False`, tout suit

La règle False.elim (l’explosion) est valide : de False, toute proposition suit, sans aucun axiome. Le danger ne vient pas de l’explosion — c’est l’axiome de secours qui fournit l’h : False qui la nourrit. Un False prouvé par sorryAx fait s’écrouler la théorie entière du notebook : tout énoncé devient prouvable.

theorem toutSuit (h : False) : (0 : Nat) = 1 := by
  exact False.elim h

#print axioms toutSuit

theorem toutSuit (h : False) : (0 : Nat) = 1 := by

  exact False.elim h

#print axioms toutSuit 'Lean35Confiance.toutSuit' does not depend on any axioms

--% env 5

Raw input

{"cmd": "theorem toutSuit (h : False) : (0 : Nat) = 1 := by\n  exact False.elim h\n\n#print axioms toutSuit\n", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "'Lean35Confiance.toutSuit' does not depend on any axioms"}],
 "env": 5}

Lecture du résultat

#print axioms toutSuit est vide : l’explosion est une règle du noyau, pas un axiome. La preuve de 0 = 1 à partir de False est honnête — ce qui est malhonnête, c’est la façon dont on a obtenu h : False. Ajoutez à cela la section 2.1 : un seul sorry transitif dans la chaîne de preuves, et tout le corpus devient de la poudre aux yeux.

3. Certificat vs headline : la fidélité de l’énoncé (p. 4-5)

Un théorème Lean est un certificat de sa formulation. La source (p. 4-5) distingue le certificat de la « headline » — la phrase qu’on vulgarise après coup : « le théorème prouve la headline » n’est jamais automatique. La formalisation peut être fidèle (elle dit exactement ce qu’elle affirme), affaiblie (elle dit moins que la headline), ou déplacée (elle dit autre chose). Et l’axe des axiomes ne dit rien de cet écart : les deux exemples suivants ont les mêmes axiomes (aucun) et des fidélités opposées.

-- Un existentiel trivialement vrai : le temoin est n'importe quel nat.
theorem ilExisteQuelqueChose : ∃ n : Nat, n = n := ⟨0, rfl⟩

-- Un existentiel qui porte un calcul : le temoin vaut 2^10.
theorem ilExisteCentVingtQuatre : ∃ n : Nat, n = 1024 := ⟨2 ^ 10, by norm_num⟩

#print axioms ilExisteQuelqueChose
#print axioms ilExisteCentVingtQuatre

-- Un existentiel trivialement vrai : le temoin est n'importe quel nat.

theorem ilExisteQuelqueChose : ∃ n : Nat, n = n := ⟨0, rfl⟩

-- Un existentiel qui porte un calcul : le temoin vaut 2^10.

theorem ilExisteCentVingtQuatre : ∃ n : Nat, n = 1024 := ⟨2 ^ 10, by norm_num⟩

#print axioms ilExisteQuelqueChose 'Lean35Confiance.ilExisteQuelqueChose' does not depend on any axioms

#print axioms ilExisteCentVingtQuatre 'Lean35Confiance.ilExisteCentVingtQuatre' depends on axioms: [propext]

--% env 6

Raw input

{"cmd": "-- Un existentiel trivialement vrai : le temoin est n'importe quel nat.\ntheorem ilExisteQuelqueChose : \u2203 n : Nat, n = n := \u27e80, rfl\u27e9\n\n-- Un existentiel qui porte un calcul : le temoin vaut 2^10.\ntheorem ilExisteCentVingtQuatre : \u2203 n : Nat, n = 1024 := \u27e82 ^ 10, by norm_num\u27e9\n\n#print axioms ilExisteQuelqueChose\n#print axioms ilExisteCentVingtQuatre\n", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "'Lean35Confiance.ilExisteQuelqueChose' does not depend on any axioms"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "'Lean35Confiance.ilExisteCentVingtQuatre' depends on axioms: [propext]"}],
 "env": 6}

Lecture du résultat

Les deux #print axioms ne diffèrent que d’un [propext] de routine (celui que norm_num introduit) — aucun axiome de secours dans les deux cas — et les deux preuves ont des fidélités opposées : le premier énoncé est une tautologie d’existence, le second contient le calcul 2 ^ 10. Les axiomes mesurent la confiance du transport — ils ne mesurent pas la fidélité de l’énoncé. C’est l’orthogonalité centrale de ce notebook : un certificat peut être sans axiome de secours et ne rien dire (section 1), ou porter un axiome légitime et dire quelque chose de précis (section 2.3). La headline d’un communiqué (« nous avons prouvé X ») se vérifie en appariant la phrase à l’énoncé, pas en relisant #print axioms.

4. Exercices

Trois exercices dans la veine des sections : raffiner une définition, lire une preuve de fausse, apparier énoncé et headline. Chaque cellule s’exécute telle quelle — la sortie du stub porte le marqueur declaration uses 'sorry' — à vous de remplacer le sorry par la vraie preuve, dont l’énoncé complet est dans le commentaire.

Exercice 1 — Raffiner la définition (p. 4)

DeuxDivise est une mis-définition : définissez le prédicat qui porte réellement la parité (∃ k, n = 2 * k), puis prouvez que 8 est divisible par 2 avec votre définition. Indice : le témoin de n = 2 * k est 4, et norm_num finit le calcul.

def DeuxDivise (_n : Nat) : Prop := True

-- TODO etudiant : remplacez la definition creuse par (∃ k : Nat, n = 2 * k).
example : DeuxDivise 8 := by
  sorry

def DeuxDivise (_n : Nat) : Prop := True

-- TODO etudiant : remplacez la definition creuse par (∃ k : Nat, n = 2 * k).

example : DeuxDivise 8 := by🟨 declaration uses `sorry`

  sorry

--% env 7

--% prove 1

Raw input

{"cmd": "def DeuxDivise (_n : Nat) : Prop := True\n\n-- TODO etudiant : remplacez la definition creuse par (\u2203 k : Nat, n = 2 * k).\nexample : DeuxDivise 8 := by\n  sorry\n", "env": 6}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 5, "column": 2},
   "goal": "⊢ Lean35Confiance.DeuxDivise 8",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 7}

Exercice 2 — Lire une preuve de fausse (p. 6)

Prouvez 1 = 2 sans aucun axiome de secours : ajoutez une hypothèse (h : False) à l’énoncé et utilisez False.elim. Relisez ensuite #print axioms : il doit être vide — c’est la signature d’une implosion nourrie par une hypothèse, pas par un sorry.

-- TODO etudiant : ajoutez la premissse (h : False) a l'enonce et eliminez-la.
example : (1 : Nat) = 2 := by
  sorry

-- TODO etudiant : ajoutez la premissse (h : False) a l'enonce et eliminez-la.

example : (1 : Nat) = 2 := by🟨 declaration uses `sorry`

  sorry

--% env 8

--% prove 2

Raw input

{"cmd": "-- TODO etudiant : ajoutez la premissse (h : False) a l'enonce et eliminez-la.\nexample : (1 : Nat) = 2 := by\n  sorry\n", "env": 7}

Raw output

{"sorries":
 [{"proofState": 2,
   "pos": {"line": 3, "column": 2},
   "goal": "⊢ 1 = 2",
   "endPos": {"line": 3, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 8}

Exercice 3 — Apparier headline et énoncé (p. 4-5)

La headline à prouver : « 1024 est une puissance de deux ». Formalisez-la honnêtement (∃ k : Nat, 1024 = 2 ^ k) et prouvez-la — le témoin est 10, et norm_num ou rfl conclut. Puis comparez le résultat de #print axioms avec celui de l’exercice 1 : fidélité et axiomes sont bien deux axes.

example : ∃ k : Nat, 1024 = 2 ^ k := by
  sorry

example : ∃ k : Nat, 1024 = 2 ^ k := by🟨 declaration uses `sorry`

  sorry

--% env 9

--% prove 3

Raw input

{"cmd": "example : \u2203 k : Nat, 1024 = 2 ^ k := by\n sorry\n", "env": 8}

Raw output

{"sorries":
 [{"proofState": 3,
   "pos": {"line": 2, "column": 2},
   "goal": "⊢ ∃ k, 1024 = 2 ^ k",
   "endPos": {"line": 2, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 9}

Conclusion : la liste de confiance

Avant de vulgariser un théorème — le sien, celui d’un lake, celui d’un outil qui annonce « prouvé formellement » —, trois questions, dans l’ordre :

La définition porte-t-elle la conclusion ? Une définition trop large (section 1) rend la preuve trivialement vraie ; #print axioms ne la détecte pas.
Quels axiomes ? Le trio attendu [propext, Classical.choice, Quot.sound] est la norme Mathlib ; un sorryAx est un trou, une confiance de réduction native un certificat par délégation. Les instruments du dépôt (count_code_sorry.py, le vérificateur proof-integrity) rendent cette lecture automatique et mesurable.
L’énoncé dit-il la headline ? Un certificat est un certificat de sa formulation, pas de la phrase du communiqué. L’orthogonalité des axes (axiomes / fidélité) est le point de ce notebook : les deux se contrôlent, aucun ne remplace l’autre.

Le kernel dit « cette preuve est valide » ; il ne dit jamais « cette preuve veut dire ce que vous annoncez ». Toute la discipline de confiance tient dans l’écart entre les deux.

Source de la piste : Dougherty et von Hippel, « Lies, Damned Lies, and Proofs — Formal Methods are not Slopless », Secure Program Synthesis blog, 2026-01-12 — exemplaire unique archivé au gisement partagé du cluster (hors dépôt).

Retour au sommet

Objectifs, prérequis et durée

1. Mis-définition : la preuve trivialement vraie (p. 4)

Lecture du résultat

Lecture du résultat

2. Axiomes de secours : les « proofs of false » (p. 6)

2.1 sorry : l’axiome de secours transitif

Lecture du résultat

2.2 native_decide : la réduction native sans preuve

Lecture du résultat

2.3 Le choix classique : légitime, mais nommé

Lecture du résultat

2.4 Implosion : une fois False, tout suit

Lecture du résultat

3. Certificat vs headline : la fidélité de l’énoncé (p. 4-5)

Lecture du résultat

4. Exercices

Exercice 1 — Raffiner la définition (p. 4)

Exercice 2 — Lire une preuve de fausse (p. 6)

Exercice 3 — Apparier headline et énoncé (p. 4-5)

Conclusion : la liste de confiance

2.1 `sorry` : l’axiome de secours transitif

2.2 `native_decide` : la réduction native sans preuve

2.4 Implosion : une fois `False`, tout suit