{"id":"hexagon/2611.00125","pdf":"https://hexagonmath.org/pdf/2611.00125v1","url":"https://hexagonmath.org/abs/2611.00125v1","tags":["math.AC","math.AG","math.AT","math.CO","math.CT","math.GN","math.GR","cs.LO","msc:68V20","msc:01A60"],"score":0,"title":"Grothendieck Montpellier. Énoncés des lectures modernisées démontrés.","domain":"math.HO","origin":"ai-generated","source":"hexagon","authors":["Michel Hua"],"reviews":0,"subject":"math.HO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["Claude Opus"],"discussed":0,"published":"2026-11-05","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":false,"human_understanding":"some"}