Example Request :: Small Algebra Project

Stream: new members

[Robert Culling]

Hello!

I've worked my way through TpiL4 to the point that I can write proofs (without using tactics). Although constructing new types is still beyond me, I think I should be able to start writing proofs of mathematical theorems.

I would find it helpful to see a small Lean4 example project that proves some theorems about (say) groups. That way I would be able to see what's required and what I am missing. Does anyone have such a project they could share with me? I realise that mathlib is such a project, but it's a little daunting to start there!

Is it "simply" a matter of downloading mathlib (Lean4) and importing the theorems needed to prove what I want to prove? Or am I missing something?

Thanks :upside_down:

[Heather Macbeth]

@Robert Culling See this file
https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/algebraic_hierarchy.lean
from the "LftCM 2020" workshop, or this chapter
https://leanprover-community.github.io/mathematics_in_lean/06_Abstract_Algebra.html
of Mathematics in Lean.

[Robert Culling]

Thank you @Heather Macbeth I'll take a look at those!

[Johan Commelin]

Note that those are Lean 3 projects. But they might still be helpful.

[Kevin Buzzard]

I should think that a fun project would be to translate them into lean 4! I learnt a lot about lean in 2017 by translating Coq code into lean

[Logan Murphy]

@Robert Culling When I was first starting out with Lean3, I started a small project formalizing very elementary group theory separate from from mathlib's algebra/group theory modules, albeit heavily guided by the constructions used in mathlib (especially the use of typeclasses). I originally wanted to formalize my own version of the first isomorphism theorem for groups, but once I got comfortable with Lean I pivoted to other work. The repository I had was here if you find it useful to take a look at (disclaimer: I was very much a novice at the time and the code may not be great quality).

I also agree with Kevin that translating something like this or the files Heather linked to lean4 is likely a great way to learn.

[Robert Culling]

@Johan Commelin thanks for the warning. I'll try and translate them :upside_down:

[Robert Culling]

I am getting trouble at the first step :upside_down:
When I write the following, Lean4 says it can't find has_mul, has_one, has_inv.

class group (G : Type) extends has_mul G, has_one G, has_inv G :=
-- and then we ask for the axioms
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

Is this because I am not importing something? or because these are not in Lean4?

Thank you!

[Arthur Paulino]

I'm not on my PC but I don't think those exist in Lean 4 by default

[Junyan Xu]

They're docs4#Mul, docs4#One, docs4#Inv in Lean 4. But in reality src4#Group extends docs4#DivInvMonoid.