Hi I am Omar Harhara, I just finished my 4th year of my integrated masters mathematics degree. In this post I will describe my experiences with Lean to date. I started learning to use Lean in September 2020 with the natural number game and mathematics in lean. For my dissertation I investigated Lean’s usefulness as a teaching tool, specifically in the context of an introductory proof course. This involved holding weekly “Proof Skills” sessions alongside James Arthur (who will also be blogging on this page). These sessions supplemented the delivery of MTH1001 – Mathematical Structures at the University of Exeter and focussed on developing proof comprehension and construction with the use of Lean. The structure of these sessions was based on student feedback. We opened the sessions with a “Pen and Paper” proof with emphasis on Lean terminology (goals, types, local context etc.) and then proceeded to exhibit the same proof and/or similar proofs in Lean after students were familiar with the concepts at hand. We found that Lean offered students an alternative perspective on the proof at hand. Students often struggle with keeping track of what remains to be proved and knowing when the proof is complete. Lean answers these questions instantly guiding students through the proof by showing the remaining goals in the tactic state. For this reason I believe Lean shows great promise as a teaching tool. This summer I will be developing Lean learning resources here.