How to learn the group theory in lean4

Stream: new members

[Marcus]

I feel very confused and helpless about group theory in Lean4, and I don't know how to get started. Is there any textbook or video that can help me quickly get started？

[Derek Rhodes]

Hi Marcus, I'm not an expert, but I am learning about groups with Lean4 at the moment. Here are some of the resources that I've found to be helpful.

⮺ Mechanics of Proof, Section 3.3 : Modular arithmetic: theory

(some group theory introductory material uses modular arithmetic, so it's good to know how to prove those types of problems)

⮺ Formalising Mathematics, Section 5 : An introduction to group theory

(Kevin Buzzard has videos that go along with these worksheets)
section 5 on github

⮺ The Lean Language Reference, Section: Subtypes

(I've found that subtypes can be helpful for representing some group examples)

⮺ Mathematics in Lean: Chapter 8.1, Monoids and Groups

(MiL has some more info on groups earlier in the book, try the search feature to find everything)

[Derek Rhodes]

There's also a convenient way to implement Cayley tables with matrices using .toCtorIdx to index the row and column.

import Mathlib

inductive L where
  | A | B | C | D
  deriving DecidableEq, Fintype
open L

instance : Mul L where
  mul a b :=
    let M := !![A, B, C, D;
                B, C, D, A;
                C, D, A, B;
                D, A, B, C]
    M a.toCtorIdx b.toCtorIdx

#eval B * B

[Marcus]

Derek Rhodes 发言道：

Hi Marcus, I'm not an expert, but I am learning about groups with Lean4 at the moment. Here are some of the resources that I've found to be helpful.

⮺ Mechanics of Proof, Section 3.3 : Modular arithmetic: theory

(some group theory introductory material uses modular arithmetic, so it's good to know how to prove those types of problems)

⮺ Formalising Mathematics, Section 5 : An introduction to group theory

(Kevin Buzzard has videos that go along with these worksheets)
section 5 on github

⮺ The Lean Language Reference, Section: Subtypes

(I've found that subtypes can be helpful for representing some group examples)

⮺ Mathematics in Lean: Chapter 8.1, Monoids and Groups

(MiL has some more info on groups earlier in the book, try the search feature to find everything)

thank you so much.