64 citations · 193 across the 24 of their papers we have counts for
29 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…
Factors of HOMFLY polynomials
Douglas Blackwell, Damiano Testa
We study factorizations of HOMFLY polynomials of certain knots and oriented links. We begin with a computer analysis of knots with at most 12 crossings, finding 17 non-trivial fact…
Complex and tropical counts via positive characteristic
Marco Pacini, Damiano Testa
We reconcile the discrepancy between the complex and tropical counts of some enumerative problems reducing to positive characteristic. Each problem that we consider suggests a prim…
On a question of Dolgachev
Marco Pacini, Damiano Testa
For each even, positive integer , we define a rational self-map on the space of plane curves of degree , using classical contravariants. In the case of plane quartics, we sho…