Lean book for mathematicians

Stream: maths

[Kevin Buzzard]

I'm writing a book for mathematicians who want to learn Lean.

[Kevin Buzzard]

Let me know what I should put in it

[Kevin Buzzard]

Of course I already have a gazillion ideas of my own

[Kevin Buzzard]

and even some stuff written -- in sphinx.

[Kevin Buzzard]

sphinx lets me write both maths and Lean code and I am happy with the results.

[Kevin Buzzard]

Curerntly it's all in a private repo

[Kevin Buzzard]

but definitely by 1st July when I have a bunch of maths UGs working with me on Lean stuff I will have made it public.

[Kevin Buzzard]

My goal is to show mathematicians that it is possible to formalise the mathematics that they are interested in, in Lean.

[Kevin Buzzard]

My target audience is undergraduates

[Kevin Buzzard]

or PhD students

[Kevin Buzzard]

but older viewers are also welcome to read it

[Kevin Buzzard]

It will be based on Lean 3.4.1 and Mathlib 3.4.1 whatever that is

[Kevin Buzzard]

(the latter is a moving target, which makes it a bit more annoying to specify succinctly)

[Johan Commelin]

I think in a chapter on tactics, you want exercises like the one you had on the semi-quasi-demi-presheaves. The exercise says: try to prove this lemma with all the tactics you have seen so far (and maybe you give an explicit list). And then the reader gets stuck (they should be warned that it is your point to get them stuck). And then you teach them a new tactic (in this case change).

[Johan Commelin]

That way, maybe we will recognise where to apply that tactic in the future. Because we will get stuck with our standard toolkit, and realise "oh, I remember this kind of stuckness from an exercise in LftWM. I need to use change!"