Making a beginner tutorial to introduce Lean to Math peoples

Stream: new members

[Oussama]

Hello everyone
it been months since i want to participate in #SoME (which a math explainer contest where you put an article or a video explaining a topic )
but two weeks ago i accidentally found Lean and i just love it , so i decide to make an article about it to motivate other math people to learn and use Lean .

I would be very grateful for your opinions on the article's structure and any suggestions you have

[Oussama]

so here the plan :

Quick introduction to formalizing theorems
then start to talk about proof assistant and lean
then start proving some problems by hand
and then rewrite them with Lean (and ofc explaining what i did step by step and show the InfoView side)
each problem will be designed to introduce a feature of Lean like :

• introduce mathlib by using defined theorems to solve our theorem
• introduce the term mode and tactic mode ( and show the InfoView while using it )
• show that Lean can catch proving mistakes by tricking the user into proving 1 = 2 by hands and get an error when trying to formalize it

then i conclude the article by chosing an IMO problem and try to formalize it with what we learned

Thank you for your time

[Martin Dvořák]

One thing to consider:
https://github.com/madvorak/read-lean

Maybe you can first teach people how to read Math written in Lean (to understand the statements), then either show them proofs or simply redirect them to NNG.

[Oussama]

@Martin Dvořák Thank you for the suggestion i tried to explain the lean code as much as possible and guide them to more learning resource at the end of the article

[Oussama]

Here is the article link if anyone is interested in reading it :
https://ouss122.github.io/Ou12Blog/blog/contradiction-contraposition-and-lean/