1 paper
Antoine Chambert-Loir, María Inés de Frutos-Fernández
The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the univers…