## Stream: maths

### Topic: Lean book for mathematicians

#### Kevin Buzzard (May 30 2018 at 13:31):

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

#### Kevin Buzzard (May 30 2018 at 13:31):

Let me know what I should put in it

#### Kevin Buzzard (May 30 2018 at 13:31):

Of course I already have a gazillion ideas of my own

#### Kevin Buzzard (May 30 2018 at 13:31):

and even some stuff written -- in sphinx.

#### Kevin Buzzard (May 30 2018 at 13:32):

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

#### Kevin Buzzard (May 30 2018 at 13:32):

Curerntly it's all in a private repo

#### Kevin Buzzard (May 30 2018 at 13:32):

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 (May 30 2018 at 13:33):

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

or PhD students

#### Kevin Buzzard (May 30 2018 at 13:33):

but older viewers are also welcome to read it

#### Kevin Buzzard (May 30 2018 at 13:33):

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

#### Kevin Buzzard (May 30 2018 at 13:34):

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

#### Johan Commelin (May 30 2018 at 14:46):

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 (May 30 2018 at 14:47):

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!"

Last updated: May 10 2021 at 07:15 UTC