Abstract: 'In traditional mathematics, many proof steps are left out and are expected to be inferred by the reader using intuition, shared context, and experience. However, proof assistants require every logical inference to be formally verified. This rigor means the verification of the proof no longer depends on these human factors.
In this talk, I will present a computable formalization of Lagrange's theorem in Lean 4. The talk will first introduce the motivation behind the computable implementation of finite group theory and explain its advantages over existing formalizations based on noncomputable notions of cardinality. Afterwards, I will discuss my implementation of the set of all left cosets and the challenges I faced when defining its cardinality as the length of a duplicate-free list of left cosets. In addition, I will talk about the techniques used to minimize dependence on axioms.'