María Inés de Frutos Fernández - Universal DP algebra

Stream: Lean Together 2026

[Markus Himmel]

Discussion thread for the talk.

[Philippe Duchon]

Purely out of curiosity: was the mistake in Roby's paper known, or was it uncovered during the formalization process?

[María Inés de Frutos Fernández]

It was certainly not widely known, but Berthelot and Ogus may have been aware of it, since their proof sketch avoids the issue (but they do not explicitly point out the mistake).