Zulip Chat Archive

Stream: new members

Topic: minor typo in mathematics in lean tutorial


view this post on Zulip Jakob Scholbach (Feb 06 2021 at 22:52):

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!

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 23:11):

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

view this post on Zulip Jakob Scholbach (Feb 07 2021 at 20:22):

thanks and no worries!

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 21:05):

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.

view this post on Zulip Jeremy Avigad (Feb 09 2021 at 00:31):

@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.


Last updated: May 18 2021 at 16:25 UTC