Structuring Definitions in Mathematical Libraries

Alena Gusakov, Peter Nelson, Stephen Watt

Codifying mathematical theories in a proof assistant or computer algebra system is a challenging task, of which the most difficult part is, counterintuitively, structuring definiti…