Mathlib initiative announcement discussion

Stream: general

[Patrick Massot]

This is the discussion thread for the Mathlib initiative announcement.

[Wrenna Robson]

There's a mention of possible jobs related to this. Would they be based somewhere in particular?

[Wrenna Robson]

I am interested (as I'm sure lots of people are) but I imagine that will make a big difference to many.

[Oliver Nash]

It is very, very early days so there's not much I can say but certainly we do plan to hire people, and we do not expect their location to be relevant.

[Oliver Nash]

I might add that I'm delighted to see a discussion thread and that we welcome questions, even if we might not yet be able to answer many of them.

[Joseph Tooby-Smith]

I have a question, which is probably down to a lack of my understanding of the terminology. How should I think of the "The Mathlib Initiative"? e.g. is it a research grant, a company, or something in between?

[Oliver Nash]

Officially / legally it is a programme of Renaissance Philanthropy. Such programmes can remain incubated in this form indefinitely or they can also evolve into an independent non-profit, say.

Practically I think it should be thought of as a group of people whose job it is to support Mathlib and the work of the Mathlib Maintainers.

[Michael Rothgang]

In terms of the categories above, is the following guess somewhat accurate?

• it's not meant to make a profit (unlike a company)
• it's not based at an academic institution (unlike most research grants)
• it will have more startup-like accountability, such as quarterly reports

(Reading this, it sounds somewhat similar to the Lean FRO --- except that one is an independent entity(not quite, see below), which the Mathlib Initiative is not, right?)

[Michael Rothgang]

Granted, it's nice to get help with doing payroll, hiring people, legal questions, etc. - spinning up all that yourself sounds like a lot of work.

[Oliver Nash]

This is all about right, modulo the detail that the Lean FRO is itself incubated within Convergent Research (albeit with a different setup that I have not studied).

[Patrick Massot]

Michael Rothgang said:

Granted, it's nice to get help with doing payroll, hiring people, legal questions, etc. - spinning up all that yourself sounds like a lot of work.

It is much more than nice, it’s 100% required. Nobody here is competent to do that or even willing to learn. This is already true for the Lean FRO. When you love all the great work that came from the FRO you also love the work done by people you don’t know at Convergent Research who made all this possible.

[Wrenna Robson]

Oliver Nash said:

It is very, very early days so there's not much I can say but certainly we do plan to hire people, and we do not expect their location to be relevant.

This is great news. To be entirely honest pending details I think "a group of people whose job it is to support Mathlib and the work of the Mathlib Maintainers" is almost precisely work I would be excited to do and very suited for - but even if that didn't work out I'm very excited that it is happening.

[Malvin Gattinger]

Here @Jason Reed said he will have more details about the available jobs soon: (See below.) https://mastodon.social/@jcreed/114937599329818056

[Patrick Massot]

Malvin, this is something completely different. Jason talks about the Lean FRO not the Mathlib Initiative.

[Malvin Gattinger]

Ohh, oops. Sorry for the confusion!

[Patrick Massot]

No problem, the situation is indeed a bit confusing. But we can’t really complain there are too many good news.

[Kim Morrison]

The connection here is that both the Mathlib Initiative and the additional hiring that Jason is organizing for the FRO's new interface work are initially funded by Alex Gerko's gifts.

[Yaël Dillies]

For future reference, the job posting is now here: #job postings > Mathlib Initiative

[Chris Hughes]

Johan Commelin said:

Although the Mathlib Initiative will work hard on reviewing PRs on the queue, it should be understood that the Mathlib maintainer team retains decision power and will remain in charge of the Mathlib library.

I'm a bit concerned about this part. I think a lot of people will not understand this distinction. The Mathlib Initiative will be the only legal entity with Mathlib in the name and I think most people will assume that it is the organization responsible for the administration of Mathlib when they first hear about it.

[Oliver Nash]

I invite people here to look at: https://github.com/mathlib-initiative/TaskList

We want to have a way for the community to communicate its needs to the Mathlib Initiative. Some remarks as follows:

• Every issue opened will be considered, even though we may not respond directly.
• Some good issues will be closed simply because they are too far outside our scope.
• There is clearly some redundancy with the issues on the main mathlib4 repo. The difference is that we commit to consider each of these issues and to triage the list regularly.