Zulip Chat Archive

Stream: maths

Topic: Lean book for mathematicians


view this post on Zulip Kevin Buzzard (May 30 2018 at 13:31):

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

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:31):

Let me know what I should put in it

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:31):

Of course I already have a gazillion ideas of my own

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:31):

and even some stuff written -- in sphinx.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:32):

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

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:32):

Curerntly it's all in a private repo

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:33):

My target audience is undergraduates

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:33):

or PhD students

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:33):

but older viewers are also welcome to read it

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 30 2018 at 13:34):

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

view this post on Zulip 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).

view this post on Zulip 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