Introduction to Lean — What is mathematics? 1.0 documentation
These pages were written for the Lean Together meeting and the target audience is mathematicians with no Lean experience at all. Watch the video and then get started on the exercises. Which bits could I explain better? What else do you need to be told in order to get going? Let me (Buzzard) know! Thanks to David Holmes and Paula Neeley for comments. This brief video might be helpful if you want to get started on the exercises. Need some basic hints about which tactics to use? Try this basic tactic guide or maybe you just want to look at a list of basic tactics. A glossary of basic words and phrases is here. This is still very light. What am I missing? To get started with these exercises, either run them online in the Lean Web Editor (maybe problems with firefox currently?) or download the Lean files directly and run them locally. Lean web editor link to sheet 1. Sheet 1 link to Lean file. Lean web editor link to sheet 2. Link to sheet 2 Lean file. I should write a .lean file, but until
Explore this link on the map →