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

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: Aug 03 2023 at 10:10 UTC