## A Formal Proof of Sylow's Theorem: An Experiment in Abstract Algebra with Isabelle HOLAbstract: "The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof is explained in some detail leading on to the mechanization of group theory and the necessary combinatorics in Isabelle. We present the mechanization of the proof in detail giving reference to theorems contained in an appendix. Some weak points of the experiment with respect to a natural treatment of abstract algebraic reasoning give rise to a discussion of the use of module systems to represent abstract algebra in theorem provers. Drawing from that, we present tentative ideas for further research into a section concept for Isabelle." |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Common terms and phrases

abstract algebra algebraic reasoning arithmetical assumptions bijection bin_op G binary operation binomial cancellation law card calM card g card(M carrier G ft choose combinatorial argument constant G coset.joinl define definition of groups derive elements equiv equivalence relation finite sets formal proof formalization of groups function G & Ml g 6 carrier G ft Ml group G group theory higher order logic induced operation instantiated invers G inverse rule Isabelle theory L. C. Paulson Lagrange's theorem lemma log p n logarithm mathematical proof max-n meta-level n_choose_n nat_rec natural number order(G prime primitive recursive function proof of Sylow's prove r.coset G M RelM ft right cosets Section set_r_cos G H subgoals subgroup H subgroup property subsets of G Sylow proof Sylow subgroup Sylow's theorem syntax theorem of Sylow theorem provers Theory File tion Wielandt