LMFDB

Stream: FLT

[Chris Birkbeck]

Hello, this is just a quick advert about the Lean--LMFDB project that we've started. The plan is to focus on formalising lots of the definitions relating to number fields, modular forms and elliptic curves. So since this is maybe also of interest to people in the FLT stream I thought I'd post a link to the #LMFDB! stream in case anyone is interested.

[Riccardo Brasca]

Nice project, I will be happy to collaborate!

[Bryan Wang]

I'd be interested to contribute!

[Chris Birkbeck]

Wonderful! There is plenty to do. I am working on a list of nice starter things, but for example there are several number field definitions that should be relatively easy to do given what we already have.

[Chris Birkbeck]

There is a WIP blueprint here

[Kevin Buzzard]

Wooah a blueprint! I would love to chat about this and I'm happy for you to advertise the project here in the FLT channel (indeed, you asked me beforehand if this was OK) but I wonder if chat would be more easily findable in a different place.

[Chris Birkbeck]

Yes so, we have a channel here: #LMFDB which we are going to use for the project, so thats maybe the natural place. It also has the added benefit of tunneling out to the LMFDB zulip channel. One of the goals is to try and bring these two communities closer together.