minor typo in mathematics in lean tutorial

Stream: new members

[Jakob Scholbach]

There seems to be a minor issue with the example : range (λ x, x^2) = {y | y ≥ 0} :=. At least when I open it in VB code, it seems to infer that x and y are natural numbers, making it impossible to prove the one inclusion.

Generally speaking, I find the tutorial quite well-done, though, kudos to the authors!

[Kevin Buzzard]

I'm sorry we haven't worked on it for months. Right now I'm generating a lot of teaching material and I'm hoping that some of it will be useful for MiL

[Jakob Scholbach]

thanks and no worries!

[Kevin Buzzard]

Because of my contractual obligations I have to teach this lean course so I'm writing maths teaching materials independent of MiL right now. I did think about just using MiL and writing more of it on the fly but then somehow this would inevitably end up with me "taking over", and I am very verbose -- I need an editor. Jeremy, Patrick and Rob on the other hand write extremely well so me taking the lead on writing would perhaps be a disaster. On the other hand where I think I can offer something useful is the experience I bring in actually working with undergraduate mathematicians on proving undergraduate level theorems in Lean. I gave a summer course last summer, I am giving this formalising-mathematics course now (leanproject get ImperialCollegeLondon/formalising-mathematics if you want to have a look, or take a look at the GitHub repo) and this material will hopefully turn into an undergraduate course next year. I'm hoping that by March I'll have an even better idea about how to present things like topological spaces to undergraduates.

[Jeremy Avigad]

@Jakob Scholbach Thanks for the kind words. Within the next week or so I plan to update MiL to the latest version of Mathlib and make sure it still builds. I see that someone addressed the issue you raised with a pull request: https://github.com/avigad/mathematics_in_lean_source/pull/38. I'll merge that too.

I am planning to return to this over the summer. There is a lot of good material we can incorporate, including stuff from the LFTCM meeting, etc. In the meanwhile, I'm happy to hear that what is there is helpful.