A modular approach to the formalisation of finite groups
Enrico Tassi, 11h –
Joint Centre + University of Bologna.
The claim of the projects is that it is possible to build reusable and easy to compose libraries of formalised mathematics and that, standing on such a solid framework, it is possible to tackle “mainstream” mathematics like the Feit-Thompson classification of finite groups of odd order. In this talk I describe some of the building blocks developed so far, focusing on the ones I worked on.