Cheking an entire book with LEAN

Stream: new members

[Luis Victoria]

Hi everybody! I¡m Luis and I recently tried Lean for the first time and I think it's amazing. I'm a math major and want to review group theory.

I was thinking, could I wrote every proof of Susuki's book using Lean? is that something possible?

I want to go as far as posiible.

[Henrik Böving]

In principle if you are sufficiently capable and bring enough time you can write proofs about any kind of mathematics in Lean. Are you asking if this is merely a thing that is possible or whether e.g. mathlib4 has theory that you can build upon?

[Luis Victoria]

The latter, I was thinking of literaly starting with the definition of groups nad start incrementaly adding new results from the book. I see that mathlb has a library for gruop theory but I don't know how extensive it is or if it's enough for a whole book

[Kevin Buzzard]

I would recommend not defining groups by yourself, but using mathlib's definition. Mathlib's definition is easy to use but very complicated under the hood, but the reason for that is precisely because it's the definition which the community think works best in Lean's type theory. If you really want to do everything from first principles then I would recommend defining your own groups, then proving that your groups are the same as lean's groups, and then using lean's groups from then onwards.

[Kevin Buzzard]

And you'd get a much better answer about the possibilities of formalising "Susuki's book" if you gave an overview of the material in the book (or a much more precise reference). Note that they formalised the whole of the Feit-Thompson odd order theorem in a theorem prover.