In this talk, we will go over what it means for an extension to be Galois. We will look at Galois and non-Galois extensions with examples. Further, we will discuss the Kronecker-Weber Theorem, which states that every finite abelian extension of \(\mathbb\) is contained in a cyclotomic field. Time permitting, we will see what happens when we look at \(\mathbb\) adjoin the division points of a curve as a field extension of \(\mathbb\).

In theory, proof assistants are a useful tool for validating mathematical claims. We will use simplicial topology as a case study to look at what goes into formalizing mathematics from pen and paper to the digital world. This is based on previous work with Stefan Friedl focused on formalizing stellar subdivisions of simplicial complexes. I will present a few anecdotal stories from our project that demonstrate some of the challenges involved. Topics include (but are not limited to) what changes when we introduce types to topology, decidability and computational complexity concerns, and what to do when the proof is left as an exercise for the reader.