4 papers
FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature Toward the Formalization of the Classification of Finite Simple Groups
Tianjiao Nie, Ao Zhang, Yusen Tang +4
Large-scale formalization of advanced mathematics requires more than translating individual statements: it must reconstruct a coherent theory distributed across heterogeneous sourc…
Fitting's Theorem and Semirings of Normal Subgroups
Damiano Testa
We define a non-unital, generally non-associative, commutative semiring structure on the collection of normal subgroups of a group . This viewpoint allows us to recast in ring-t…
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for ch…
The surface parametrizing cuboids
Michael Stoll, Damiano Testa
We study the surface parametrizing cuboids: it is defined by the equations relating the sides, face diagonals and long diagonal of a rectangular box. It is an open proble…