Zulip Chat Archive

Stream: new members

Topic: Example Request :: Small Algebra Project

Robert Culling (Jan 06 2023 at 01:53):


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 (Jan 06 2023 at 01:56):

@Robert Culling See this file
from the "LftCM 2020" workshop, or this chapter
of Mathematics in Lean.

Robert Culling (Jan 06 2023 at 02:29):

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

Johan Commelin (Jan 06 2023 at 05:43):

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

Kevin Buzzard (Jan 06 2023 at 06:52):

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 (Jan 06 2023 at 15:20):

@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 (Jan 08 2023 at 23:39):

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

Robert Culling (Jan 13 2023 at 02:08):

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 (Jan 13 2023 at 03:57):

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

Junyan Xu (Jan 13 2023 at 04:24):

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

Last updated: Dec 20 2023 at 11:08 UTC