math.HO — History and Overview
Grothendieck Montpellier. Énoncés des lectures modernisées démontrés.
Working notes of Alexandre Grothendieck, put online by the University of Montpellier, have been transcribed and restated in current notation with a language model; the restatements may contain errors. This appendix proves statements taken from these restatements in seventy-five folders, in commutative algebra, algebraic geometry, plane affine geometry, general and tame topology, category and group theory, homotopical algebra, order theory, algebra and finite combinatorics. Each proof follows a proof checked in the Lean 4 proof assistant with its library mathlib. For each statement the text gives the context of the leaf, the proof, the hypotheses that are superfluous or necessary, and the corrections made to the restatement or to the page. It ends with the list of statements the sections report without a Lean check.