% Engendré par recapitulatif.mjs : ne pas modifier à la main.
\section*{Tableau récapitulatif}\addcontentsline{toc}{section}{Tableau récapitulatif}

Une ligne par section, dans l'ordre des parties : la cote, l'énoncé démontré en quelques mots, le verdict, le fichier Lean et la section. \emph{Confirmé tel que lu} : l'énoncé tient sous les hypothèses que la lecture écrit ; \emph{plus général} : il tient sous des hypothèses plus faibles ; \emph{partiel} : une partie seulement est démontrée, ou dans un modèle, ce que la section précise ; \emph{correction de la lecture} : la lecture omettait une hypothèse de la page ou glosait faussement un énoncé juste ; \emph{faux sur la page} : un contre-exemple réfute une affirmation du feuillet ; \emph{conjecture de la page réfutée} : de même pour ce que le feuillet présume sans l'affirmer ; \emph{déjà dans mathlib} : l'énoncé y figure, et le fichier Lean ne fait que l'y rapporter. Une section qui démontre plusieurs énoncés peut porter plusieurs verdicts.

\begin{landscape}
{\small\setlength{\tabcolsep}{4pt}
\begin{longtable}{@{}>{\raggedright\arraybackslash}p{1.8cm}>{\raggedright\arraybackslash}p{12cm}>{\raggedright\arraybackslash}p{3.4cm}p{3.4cm}r@{}}
\toprule
Cote & Énoncé & Verdict & Fichier Lean & \S\\
\midrule
\endhead
\multicolumn{5}{@{}l}{\textit{Cycles algébriques et conjectures standard}}\\[1pt]
11 & La sous-algèbre tautologique des puissances de X, un modèle algébrique & partiel & \href{\leanblob/Folder11.lean}{\texttt{\detokenize{Folder11}}} & \ref{sec:11}\\
16 & Le pseudo-inverse de l'opérateur de Lefschetz, la normalisation de sl(2) et les algèbres de Hodge & partiel ; correction de la lecture (glose fausse) & \href{\leanblob/Folder16.lean}{\texttt{\detokenize{Folder16}}} & \ref{sec:16}\\
98 & Une théorie axiomatique des normes, le modèle des G-ensembles ; classes de faisceaux & partiel & \href{\leanblob/Folder98.lean}{\texttt{\detokenize{Folder98}}} & \ref{sec:98}\\
\multicolumn{5}{@{}l}{\textit{Théorie de Hodge}}\\[1pt]
13 & La question du double réseau et le cas de Tate & partiel & \href{\leanblobmain/Folder13.lean}{\texttt{\detokenize{Folder13}}} & \ref{sec:13}\\
\multicolumn{5}{@{}l}{\textit{Algèbre universelle et théories}}\\[1pt]
161-2 & Monadicité, caractérisation de Gabriel--Ulmer & partiel & \href{\leanblob/Folder161_2.lean}{\texttt{\detokenize{Folder161_2}}} & \ref{sec:161-2}\\
\multicolumn{5}{@{}l}{\textit{Analyse fonctionnelle}}\\[1pt]
1 & Le système d'inégalités des valeurs singulières, coefficients de Fredholm & partiel & \href{\leanblob/Folder1.lean}{\texttt{\detokenize{Folder1}}} & \ref{sec:1}\\
113 & L'enveloppe de Karoubi et l'invariance de Morita & partiel & \href{\leanblob/Folder113.lean}{\texttt{\detokenize{Folder113}}} & \ref{sec:113}\\
\multicolumn{5}{@{}l}{\textit{Théorie de la dualité}}\\[1pt]
43 & Polynômes additifs modulo $F - 1$ et perfection & partiel & \href{\leanblob/Folder43.lean}{\texttt{\detokenize{Folder43}}} & \ref{sec:43}\\
101 & La dualité locale en dimension un pour tous les modules & confirmé tel que lu & \href{\leanblob/Folder101.lean}{\texttt{\detokenize{Folder101}}} & \ref{sec:101}\\
125 & La carte des équivalences et le lemme du feuillet III-18 & partiel & \href{\leanblob/Folder125.lean}{\texttt{\detokenize{Folder125}}} & \ref{sec:125}\\
115 & La dualité d'Isbell par le calcul des noyaux & confirmé tel que lu & \href{\leanblob/Folder115.lean}{\texttt{\detokenize{Folder115}}} & \ref{sec:115}\\
\multicolumn{5}{@{}l}{\textit{Descente}}\\[1pt]
128 & Descente le long d'un conducteur nilpotent, idéaux d'équivalence de rang deux & partiel & \href{\leanblob/Folder128.lean}{\texttt{\detokenize{Folder128}}} & \ref{sec:128}\\
\multicolumn{5}{@{}l}{\textit{Topos et sites}}\\[1pt]
161-3 & Le topos d'un produit d'espaces & partiel ; confirmé tel que lu & \href{\leanblobmain/Folder161_3.lean}{\texttt{\detokenize{Folder161_3}}} & \ref{sec:161-3}\\
37 & Le contre-exemple à EGA I 10.10.5 & plus général & \href{\leanblob/Folder37.lean}{\texttt{\detokenize{Folder37}}} & \ref{sec:37}\\
\multicolumn{5}{@{}l}{\textit{Variétés abéliennes et schémas de Picard}}\\[1pt]
44 & L'intégralité des nombres de Cartan à partir des axiomes & correction de la lecture (glose fausse) & \href{\leanblob/Folder44.lean}{\texttt{\detokenize{Folder44}}} & \ref{sec:44}\\
50 & La formule des traces dans le cadre axiomatique & correction de la lecture (hypothèse omise) & \href{\leanblob/Folder50.lean}{\texttt{\detokenize{Folder50}}} & \ref{sec:50}\\
63 & Les quatre composantes de $j = 0$ ont quatre tangentes en $p = 2$ & faux sur la page (contre-exemple) ; correction de la lecture (glose fausse) & \href{\leanblob/Folder63.lean}{\texttt{\detokenize{Folder63}}} & \ref{sec:63}\\
100 & Un point de dimension un hors d'une famille dénombrable de diviseurs & partiel & \href{\leanblob/Folder100.lean}{\texttt{\detokenize{Folder100}}} & \ref{sec:100}\\
\multicolumn{5}{@{}l}{\textit{Catégories tensorielles et dualité tannakienne}}\\[1pt]
155 & Le produit de Takeuchi comme quotient d'un idéalisateur & partiel & \href{\leanblob/Folder155.lean}{\texttt{\detokenize{Folder155}}} & \ref{sec:155}\\
\multicolumn{5}{@{}l}{\textit{Algèbre commutative}}\\[1pt]
21 & Injectifs de $I$-torsion, critère ponctuel pour un champ & partiel & \href{\leanblob/Folder21.lean}{\texttt{\detokenize{Folder21}}} & \ref{sec:21}\\
22 & Produits de modules plats (lemme 3.3, corollaires 3.4 et 3.5), l'obstruction sur {$k[[t]]$}, un noyau de différentielles & partiel & \href{\leanblob/Folder22.lean}{\texttt{\detokenize{Folder22}}} & \ref{sec:22}\\
IHÉS SGA\,6 1/5 & Modules à $n$-présentation finie & confirmé tel que lu ; plus général & \href{\leanblobmain/IhesSGA6_1_5.lean}{\texttt{\detokenize{IhesSGA6_1_5}}} & \ref{sec:ihes-sga6-1-5}\\
67 & Modules à involution et triples (P, Q, m) & plus général & \href{\leanblob/Folder67.lean}{\texttt{\detokenize{Folder67}}} & \ref{sec:67}\\
\multicolumn{5}{@{}l}{\textit{Catégories et foncteurs}}\\[1pt]
19 & Le théorème de comonadicité 1.12, la comonade sur une base produit le théorème de Gabriel--Popescu et les chaînes d'adjoints & partiel ; faux sur la page (contre-exemple) & \href{\leanblob/Folder19.lean}{\texttt{\detokenize{Folder19}}} & \ref{sec:19}\\
133 & Le centre et le groupe dérivé vus par deux modules croisés & partiel & \href{\leanblob/Folder133.lean}{\texttt{\detokenize{Folder133}}} & \ref{sec:133}\\
161-1 & La partie fixe d'une adjonction, les adjonctions idempotentes, les objets locaux & plus général & \href{\leanblob/Folder161_1.lean}{\texttt{\detokenize{Folder161_1}}} & \ref{sec:161-1}\\
\multicolumn{5}{@{}l}{\textit{Géométrie formelle, modules et représentabilité}}\\[1pt]
39 & Le théorème de préparation « formel » ; fonctions implicites dans une classe de séries & plus général & \href{\leanblob/Folder39.lean}{\texttt{\detokenize{Folder39}}} & \ref{sec:39}\\
41 & Continuité de la section générique et ouverture (proposition 1) & plus général & \href{\leanblob/Folder41.lean}{\texttt{\detokenize{Folder41}}} & \ref{sec:41}\\
42 & Familles cohérentes de germes, le lemme 1 et le lemme 2 & plus général & \href{\leanblob/Folder42.lean}{\texttt{\detokenize{Folder42}}} & \ref{sec:42}\\
\multicolumn{5}{@{}l}{\textit{K-théorie, classes de Chern et Riemann--Roch}}\\[1pt]
2 & Une classe non nulle de classe de Chern totale triviale & partiel & \href{\leanblob/Folder2.lean}{\texttt{\detokenize{Folder2}}} & \ref{sec:2}\\
IHÉS SGA\,6 2/3 & Le groupe $K$ d'une catégorie triangulée, la formule d'Euler & confirmé tel que lu ; partiel & \href{\leanblobmain/IhesSGA6_2_3.lean}{\texttt{\detokenize{IhesSGA6_2_3}}} & \ref{sec:ihes-sga6-2-3}\\
153 & Polynômes à valeurs entières, co-opérations, analyseurs & plus général ; partiel & \href{\leanblob/Folder153.lean}{\texttt{\detokenize{Folder153}}} & \ref{sec:153}\\
\multicolumn{5}{@{}l}{\textit{Cohomologie cristalline et de de Rham}}\\[1pt]
5 & L'algèbre artinienne universelle à puissances divisées & partiel & \href{\leanblob/Folder5.lean}{\texttt{\detokenize{Folder5}}} & \ref{sec:5}\\
\multicolumn{5}{@{}l}{\textit{Schémas en groupes et groupes algébriques}}\\[1pt]
10 & Les indécomposables de $\mathbb G_a \rtimes \mathbb G_m$ & partiel & \href{\leanblob/Folder10.lean}{\texttt{\detokenize{Folder10}}} & \ref{sec:10}\\
90 & Un groupe plat irréductible dont un saturé n'est pas de type fini & faux sur la page (contre-exemple) & \href{\leanblob/Folder90.lean}{\texttt{\detokenize{Folder90}}} & \ref{sec:90}\\
40 & La régularité des torseurs sous α\_p ne passe pas à la somme & plus général & \href{\leanblob/Folder40.lean}{\texttt{\detokenize{Folder40}}} & \ref{sec:40}\\
46 & Relever un cocycle à travers la réduction modulo $\mathfrak m$ & partiel & \href{\leanblob/Folder46.lean}{\texttt{\detokenize{Folder46}}} & \ref{sec:46}\\
53 & Un monoïde simplifiable est un groupe & partiel & \href{\leanblob/Folder53.lean}{\texttt{\detokenize{Folder53}}} & \ref{sec:53}\\
78 & Le critère de fermeture des polygones réguliers sur un anneau, et les 2p-gones en bande & plus général & \href{\leanblob/Folder78.lean}{\texttt{\detokenize{Folder78}}} & \ref{sec:78}\\
64 & La configuration octaédrale en caractéristique 5 & plus général & \href{\leanblob/Folder64.lean}{\texttt{\detokenize{Folder64}}} & \ref{sec:64}\\
80 & Un contre-exemple au théorème des arrangements cruciaux & faux sur la page (contre-exemple) & \href{\leanblob/Folder80.lean}{\texttt{\detokenize{Folder80}}} & \ref{sec:80}\\
82 & $\mathfrak{sl}(2)$ et la conique en caractéristique 2, cas déployé & partiel & \href{\leanblob/Folder82.lean}{\texttt{\detokenize{Folder82}}} & \ref{sec:82}\\
84 & Le produit des algèbres quadratiques, en coordonnées & partiel & \href{\leanblob/Folder84.lean}{\texttt{\detokenize{Folder84}}} & \ref{sec:84}\\
160 & Le déterminant de Moore et les coefficients de Dickson & confirmé tel que lu ; faux sur la page (contre-exemple) & \href{\leanblob/Folder160.lean}{\texttt{\detokenize{Folder160}}} & \ref{sec:160}\\
69 & Les automorphismes du graphe des vingt-sept droites qui fixent un triangle & partiel & \href{\leanblob/Folder69.lean}{\texttt{\detokenize{Folder69}}} & \ref{sec:69}\\
89 & La relation fondamentale en rang deux & plus général & \href{\leanblobmain/Folder89.lean}{\texttt{\detokenize{Folder89}}} & \ref{sec:89}\\
\multicolumn{5}{@{}l}{\textit{Surfaces de Riemann, uniformisation et modules des courbes}}\\[1pt]
93 & La différence schwarzienne en dérivées divisées & partiel & \href{\leanblob/Folder93.lean}{\texttt{\detokenize{Folder93}}} & \ref{sec:93}\\
\multicolumn{5}{@{}l}{\textit{Champs, gerbes et catégories fibrées}}\\[1pt]
62 & L'invariant $j$ d'une conique munie d'une trisection étale & partiel & \href{\leanblob/Folder62.lean}{\texttt{\detokenize{Folder62}}} & \ref{sec:62}\\
\multicolumn{5}{@{}l}{\textit{Topologie combinatoire, surfaces et cartes}}\\[1pt]
152 & Le dictionnaire des graphes circularisés et des contours & partiel & \href{\leanblob/Folder152.lean}{\texttt{\detokenize{Folder152}}} & \ref{sec:152}\\
88 & L'ordre $2\nu$ et la trichotomie des cartes standard & partiel & \href{\leanblob/Folder88.lean}{\texttt{\detokenize{Folder88}}} & \ref{sec:88}\\
73 & Les aires des oreilles d'un polygone plan & confirmé tel que lu & \href{\leanblob/Folder73.lean}{\texttt{\detokenize{Folder73}}} & \ref{sec:73}\\
74 & Complexes cubiques généralisés, la réduction à un carré latin et à ses revêtements doubles & correction de la lecture (hypothèse omise) & \href{\leanblob/Folder74.lean}{\texttt{\detokenize{Folder74}}} & \ref{sec:74}\\
76 & L'ordre des sommets ; drapeaux de type H, le lemme de surjectivité & confirmé tel que lu & \href{\leanblob/Folder76.lean}{\texttt{\detokenize{Folder76}}} & \ref{sec:76}\\
77 & Le discriminant universel modulo 2 et modulo 4, la sphère, la symétrie canonique & plus général & \href{\leanblob/Folder77.lean}{\texttt{\detokenize{Folder77}}} & \ref{sec:77}\\
79 & Graphes à homothéties, commutant et étoiles sur $(\mathbf Z/n)^2$ & plus général & \href{\leanblob/Folder79.lean}{\texttt{\detokenize{Folder79}}} & \ref{sec:79}\\
85 & Représentations de $G_2$ et de $\mathbb D_\infty$ dans $\mathrm{PGL}_2$, rotation d'ordre 5 & partiel & \href{\leanblob/Folder85.lean}{\texttt{\detokenize{Folder85}}} & \ref{sec:85}\\
\multicolumn{5}{@{}l}{\textit{Jeux et combinatoire}}\\[1pt]
68 & Les théories de l'orientation et leurs applications de Stokes & confirmé tel que lu & \href{\leanblob/Folder68.lean}{\texttt{\detokenize{Folder68}}} & \ref{sec:68}\\
\multicolumn{5}{@{}l}{\textit{Groupes fondamentaux et théorie de Galois}}\\[1pt]
29 & Le critère du déterminant sur l'inertie modérée & confirmé tel que lu & \href{\leanblob/Folder29.lean}{\texttt{\detokenize{Folder29}}} & \ref{sec:29}\\
145 & L'exposant unité dans le groupe profini libre & plus général & \href{\leanblob/Folder145.lean}{\texttt{\detokenize{Folder145}}} & \ref{sec:145}\\
\multicolumn{5}{@{}l}{\textit{Polyèdres et géométrie convexe}}\\[1pt]
70 & L'icosaèdre en coordonnées universelles, fidèle en toute caractéristique, et sa conique modulo 5 & partiel & \href{\leanblob/Folder70.lean}{\texttt{\detokenize{Folder70}}} & \ref{sec:70}\\
86 & Les cinq trièdres de l'icosaèdre et l'icosaèdre gauche & confirmé tel que lu & \href{\leanblob/Folder86.lean}{\texttt{\detokenize{Folder86}}} & \ref{sec:86}\\
72 & Réalisations par pseudo-réflexions d'un polytope régulier & partiel & \href{\leanblob/Folder72.lean}{\texttt{\detokenize{Folder72}}} & \ref{sec:72}\\
\multicolumn{5}{@{}l}{\textit{Théorie de l'homotopie et catégories tests}}\\[1pt]
136 & Le lemme binomial des ombres & plus général & \href{\leanblob/Folder136.lean}{\texttt{\detokenize{Folder136}}} & \ref{sec:136}\\
106 & Catégories à cofibrations, factorisation de Brown et critère $(\star\star)$ & plus général & \href{\leanblob/Folder106.lean}{\texttt{\detokenize{Folder106}}} & \ref{sec:106}\\
114 & Les localisateurs fondamentaux et la proposition 4 & correction de la lecture (hypothèse omise) & \href{\leanblob/Folder114.lean}{\texttt{\detokenize{Folder114}}} & \ref{sec:114}\\
118 & Produits stables sans asphéricité & confirmé tel que lu ; faux sur la page (contre-exemple) & \href{\leanblob/Folder118.lean}{\texttt{\detokenize{Folder118}}} & \ref{sec:118}\\
158 & Monoïdes finis, monoïdes à élément minimal, catégories finies & correction de la lecture (glose fausse) ; faux sur la page (contre-exemple) & \href{\leanblob/Folder158.lean}{\texttt{\detokenize{Folder158}}} & \ref{sec:158}\\
104 & Catégories de modèles, trois exemples, épinglages, un complexe globulaire & partiel & \href{\leanblob/Folder104.lean}{\texttt{\detokenize{Folder104}}} & \ref{sec:104}\\
\multicolumn{5}{@{}l}{\textit{Topologie modérée et espaces stratifiés}}\\[1pt]
121 & La décomposition cellulaire admissible la plus grossière & confirmé tel que lu & \href{\leanblob/Folder121.lean}{\texttt{\detokenize{Folder121}}} & \ref{sec:121}\\
120 & Sommes amalgamées, écraser une partie modérée sur un corps & plus général & \href{\leanblob/Folder120.lean}{\texttt{\detokenize{Folder120}}} & \ref{sec:120}\\
150 & Voisinages coniques, un contre-exemple sur {[0, 1]} & faux sur la page (contre-exemple) & \href{\leanblob/Folder150.lean}{\texttt{\detokenize{Folder150}}} & \ref{sec:150}\\
\multicolumn{5}{@{}l}{\textit{Géométrie anabélienne et dessins}}\\[1pt]
146 & Les exposants trivialisants de $L_i$ et de $L$ sur $M_{0,n}$ & partiel & \href{\leanblob/Folder146.lean}{\texttt{\detokenize{Folder146}}} & \ref{sec:146}\\
140-1 & Le groupe $H^1(U_{0,3}, \mathfrak S_3; \mathbf G_m)$ & partiel & \href{\leanblob/Folder140_1.lean}{\texttt{\detokenize{Folder140_1}}} & \ref{sec:140-1}\\
\multicolumn{5}{@{}l}{\textit{Ordres et géométrie des formes}}\\[1pt]
156-1 & Le modèle-segment est un biordre & confirmé tel que lu & \href{\leanblob/Folder156_1.lean}{\texttt{\detokenize{Folder156_1}}} & \ref{sec:156-1}\\
156-2 & Les rives d'une partie fermée & partiel & \href{\leanblob/Folder156_2.lean}{\texttt{\detokenize{Folder156_2}}} & \ref{sec:156-2}\\
156-3 & L'intermédiarité se lit sur les découpages & confirmé tel que lu & \href{\leanblob/Folder156_3.lean}{\texttt{\detokenize{Folder156_3}}} & \ref{sec:156-3}\\
156-4 & Les parties saturées ne forment pas une algèbre de Boole & conjecture de la page réfutée & \href{\leanblob/Folder156_4.lean}{\texttt{\detokenize{Folder156_4}}} & \ref{sec:156-4}\\
\bottomrule
\end{longtable}}
\end{landscape}