---
Marco Maggesi (Università di Firenze), Explaining Universal Algebra to the computer: Formal Foundations and Emerging Directions
Abstract: Universal algebra reveals the common language behind mathematical structures such as groups, rings, and lattices by describing them solely through operations and equations. The first half of this talk surveys how those ideas have been formalised in proof assistants. The second half turns to ongoing work in univalent foundations: we show how displayed universal algebras, recently implemented in UniMath, assemble complex structures layer-by-layer and open new avenues for constructive mathematics and reusable code. The aim is an accessible overview linking classical intuition with cutting-edge formal tools.
Pierluigi Graziani (Università di Urbino Carlo Bo), How Heavy Is a Light-Looking Proof? Towards a Readability Criterion for Humans and Machines
Abstract: Previous research has explored criteria for evaluating the simplicity and readability of geometric proofs generated by theorem provers, primarily from a human perspective. In particular, Graziani and Quaresma (2023) examined the simplicity and readability of proofs produced by theorem provers implementing the area method, introducing Geometrographic coefficients to quantify various aspects of proof complexity. Building upon their work, this study extends the analysis by investigating the computational effort involved in the proof process, specifically by measuring CPU time. The objective is to determine whether, within the context of proof generation, the hypothesised human effort corresponds with the machine’s measured computational workload. This comparison might offer valuable insights into improving the readability of machine-generated proofs by jointly taking human cognitive constraints and computational limitations into account.