AI for Math fund projects

Stream: general

[Kim Morrison]

See the announcement about the first 29 grant awards at #announce > AI for Math fund announcements @ 💬 .

[Kim Morrison]

Of those 29, 14 17! explicitly mention Lean in their abstracts, and I'm sure a few more are planning to use Lean! :-)

[Kim Morrison]

I was really excited to see that nearly all of the Lean projects have participants with accounts here on the Zulip. :-)

[Siddhartha Gadgil]

@Kim Morrison
You seem to have missed LeanAide and LeanTutor (both mentioning Lean in the title :smile:).

[Leni Aniva]

Seems like RenPhil made changes to our proposal's text before publishing it on their webpage.

[Pawan sasanka ammanamanchi]

Not mentioned in the abstract, but a big part of our project as well

[Kim Morrison]

Siddhartha Gadgil said:

Kim Morrison
You seem to have missed LeanAide and LeanTutor (both mentioning Lean in the title :smile:).

Oh dear! I think was opening tabs to read the abstracts, and then made the list from my open tabs, but then forgot to add the ones that were so obviously using Lean that I didn't need to open the tab! :-)

[Kim Morrison]

Prompted by a request for exactly this from one team: please let the Zulip admin team know, e.g. here in this thread or by DM, if you would like a channel in the "projects" folder associated with your project, whether for private use by the team members or interaction with the wider Lean community.

(Per usual leanprover zulip policy, any private channels must have a nominated moderator who undertakes to raise any code of conduct issues with the code of conduct team if necessary.)

[Chris Birkbeck]

So let me use this stream to take the opportunity to say that @David Roe, @Andrew Sutherland and I are kicking off a project to build connections between the LMFDB and Mathlib. Our first priority on the Mathlib side is to add definitions for the objects that show up in the LMFDB (focused at first on elliptic curves, number fields and modular forms). We have a newly created (rough) blueprint, built out of the LMFDB's knowls and will be working to flesh that out over the coming months.

If you are interested in getting involved, check out the announcement for more details and join us at #LMFDB!

[Chris Birkbeck]

As a part of this, @David Ang will also be working on the project. Mainly on the elliptic curve side of things.

[Marcus Rossel]

Kim Morrison said:

Prompted by a request for exactly this from one team: please let the Zulip admin team know, e.g. here in this thread or by DM, if you would like a channel in the "projects" folder associated with your project, whether for private use by the team members or interaction with the wider Lean community.

(Per usual leanprover zulip policy, any private channels must have a nominated moderator who undertakes to raise any code of conduct issues with the code of conduct team if necessary.)

Is this available only for announced projects, or also for what one might consider personal projects / internal collaborations? And if so, who are the admins to contact?

[Patrick Massot]

In the Zulip menu (the gears icon), there is an item “Organization settings” with a “Users” tab where you can filter users by role, including the admin role.

[Patrick Massot]

There you should see
image.png