Zulip Chat Archive
Stream: general
Topic: Dawn of Formalized Mathematics
Johan Commelin (Jun 26 2021 at 05:31):
@Andrej Bauer gave a talk at the 8th European Congress of Mathematics. See also http://math.andrej.com/2021/06/24/the-dawn-of-formalized-mathematics/ for slides and a video recording.
Yaël Dillies (Jun 26 2021 at 07:59):
Features a lovely animation of us contributing to mathlib!
Eric Wieser (Jun 26 2021 at 08:21):
What's the timestamp to skip to that animation?
Riccardo Brasca (Jun 26 2021 at 08:23):
It is around the 39th minute
Patrick Massot (Jun 26 2021 at 09:12):
With again the now classical: "mathlib is the project led by Kevin Buzzard"...
Patrick Massot (Jun 26 2021 at 09:17):
And then he goes on to say that the liquid tensor experiment challenge was mostly addressed to the Lean community. This is completely wrong, and I think it's important. Everybody was welcome to try. As far as I know other communities simply weren't interested. They are interested in other things.
Kevin Buzzard (Jun 26 2021 at 10:34):
There's not a lot one can do about the random attribution. I'd misunderstood. I thought Johan told me that he'd said LTE was led by me :-/ I've put him right about this once on Twitter already.
Patrick Massot (Jun 26 2021 at 10:35):
I know it's not your fault Kevin. We should still fight back. I wrote an email already.
Kevin Buzzard (Jun 26 2021 at 10:43):
I don't think the first blog post mentions lean specifically at all, it was just a challenge to the general community as far as I could see
Mario Carneiro (Jun 26 2021 at 11:50):
The fact that it was posted on the blog of someone who usually blogs about lean probably influenced the outcome though
Patrick Massot (Jun 26 2021 at 11:53):
In retrospect it would have been much better to post this on Peter's website, and simply put a link from Kevin's blog to Peter's website. But Peter's website is on the sober side of websites.
David Renshaw (Jun 26 2021 at 12:18):
I love this part of the talk:
This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.
Adam Topaz (Jun 26 2021 at 14:31):
Andrej posted a video of just the mathlib animation here:
Filippo A. E. Nuccio (Jun 27 2021 at 10:44):
I have just seen the video of his talk, it is great!
Heather Macbeth (Jun 27 2021 at 16:56):
It is a really nice video! Perhaps we could borrow it for the community website? maybe on
https://leanprover-community.github.io/contribute/index.html
or
https://leanprover-community.github.io/meet.html
Jason Rute (Jun 27 2021 at 18:02):
I think he just used this tool or similar: https://gource.io
Jason Rute (Jun 27 2021 at 18:02):
To make the animation that is.
Mario Carneiro (Jun 28 2021 at 15:29):
yes that's a gource video
Mario Carneiro (Jun 28 2021 at 15:31):
we made something similar for metamath a while back: https://www.youtube.com/watch?v=LVGSeDjWzUo . As I understand it's pretty simple to set up, you just point it to a git repo and it uses commit data to make a nice visualization
Last updated: Dec 20 2023 at 11:08 UTC