Theorems proved using the Lean prover.

First Sylow Theorem is proved for finite group theory. The machine checked proof follows the prose style proof sketched here.

Group theory is now available as a part of the Lean standard library.