Statement on my resignation as a maintainer

Stream: general

[Chris Hughes]

Last year I resigned as a mathlib maintainer. I did not make clear my reasons for resigning at the time and I will say something about my reasons now.

The reason is principally because of a conduct issue. I won't go into too much detail about this issue. I have spoken to the code of conduct team and they did not take action to resolve the problem.

I think that improvements need to be made to mathlib's approach to code of conduct.

• It is a very bad idea for code of conduct issues to be handled by people too close to the people involved in the complaint, in particular when warnings have been made about the consequences of taking a stand or speaking out. I don't think that having more senior people on the team would fix this problem.

• The scope of the code of conduct needs to be made clear. Much of what took place did not happen on GitHub or Zulip. The warnings that I have received about what might happen in future are also likely referring to things that may happen outside of GitHub and Zulip. Some open source projects have a very broad scope for their code of conduct. Mathlib needs to decide what its scope should be.

• There needs to be a clear distinction between the personal opinions of individuals and the community's officially enforced stance.

Now that mathlib has become a much larger project, and a project without serious competitors, there are going to be more competing interests involved. I consider the problems I have faced to be basically an issue of competing interests. For this reason I think mathlib needs clear goals and values. There will be internal and external pressure to go against these values, and the community needs to be able to resist that, and right now I don't think it can. I don't have all the answers here, and I know this is not an easy problem, but I think it will make a huge difference to the future of mathlib to take this sort of issue seriously.

[Jeremy Tan]

OK, so what do I need to do about this?

[Jeremy Tan]

Personally this reminds me of the Monica Cellio case on Stack Exchange. I have always believed that changing your username to say "Reinstate Monica", "SE is evil", etc. is a plain dumb idea

[Jeremy Tan]

Nevertheless I will propose a couple of improvements to the code of conduct process:

• The scope of the CoC is everything related to mathlib – both online and offline spaces. This was taken from the Wikimedia Foundation's CoC (historically I edited Wikipedia articles, all the way back in the early 2010s).
• None of the enforcers of the code of conduct (e.g. arbitrators) can be a maintainer themselves.

[Floris van Doorn]

@Chris Hughes On behalf of the maintainer team, thank you for your suggestions; we will discuss them at the next maintainers meeting. Not only the code of conduct team but also several members of the maintainers team have tried to address your concerns, and we are sorry that you are not satisfied with the responses. The Lean Community platforms are not the place to litigate personal grievances or settle external disputes, and there is only so much we can do to resolve them. We will continue to do everything we can to keep these platforms a safe and welcoming environment for everyone.

[Chris Hughes]

Can I just reiterate my first point

Chris Hughes said:

It is a very bad idea for code of conduct issues to be handled by people too close to the people involved in the complaint, in particular when warnings have been made about the consequences of taking a stand or speaking out.

I am not interested in asking for a verdict from the community about my particular case. If I do ever ask for a verdict from the community, it will only be if I can present all the evidence in confidence to people who aren't at risk of retaliation and so on.

The purpose of this message was to ensure that the community does have a realistic strategy for dealing with conduct problems, and not just my own. Most people in my situation would not make public statements like mine, they would leave silently. There needs to be a real plan that people have confidence in, that doesn't require people to make this sort of public pressure.

[Bulhwi Cha]

I'm not sure what happened, but I'd like to know what this "real plan" could be.

[Chris Hughes]

So I think that's a complicated problem, and I'll try to answer it while keeping this discussion theoretical. I do think that the solution goes a long way beyond rules and enforcement. I don't think I'm qualified to fully answer this question. I do not think it's something that's going to be fixed overnight.

I think expectations need to be much clearer. People involved were often simply following what seemed to be the best path to stay of trouble.

I think serious attention needs to be paid to the question of who is in charge and how is that power exercised. Ostensibly we have an admin team, but I don't think every voice on that team has equal weight.

I think that external factors have a huge impact on whether mathlib is a safe and welcoming environment. In order to have a career in formalized mathematics as a mathlib contributor you need to be able to attend conferences, publish papers, get qualifications and so on. This may or may not be the responsibility of the maintainers, but it's certainly something that anybody who wants the community to do well needs to pay attention to.

I don't think the responsibility for this lies solely with the maintainers. Part of the purpose of going public is that the community would just pay more attention to questions of management and culture. Another purpose of speaking out is to empower other people who have go through similar things; it will be harder to blame people for what's happening to them if other people have been through similar things.

[Jeremy Ravenel]

"and a project without serious competitors"

I might like to challenge that some. There are mamy small projects with carefully defined goals- not unserious, but instead with a smaller scope.

[Chris Hughes]

Jeremy Ravenel said:

"and a project without serious competitors"

I might like to challenge that some. There are mamy small projects with carefully defined goals- not unserious, but instead with a smaller scope.

I agree, but I think it's fair to say that for some fields of mathematics, mathlib is the only reasonable choice. The reason I mentioned that is because this has an effect on the culture in two ways. It means that the success of the project can be a less important individual motivation. It also means that the cost of taking a risk and expressing an unpopular opinion or rocking the boat in some way is much higher because there's nowhere else to go.

[Bulhwi Cha]

I know it's hard, but some people may want to create an alternative.

[Ruben Van de Velde]

I don't think fracturing the ecosystem would be a good outcome. That does mean we need to take extra care with governance, of course

[Bulhwi Cha]

Alternative libraries wouldn't necessarily fracture the ecosystem. Some formalizers might want to create libraries that choose unique approaches to formalized mathematics. Those libraries could explore methods or subjects that Mathlib doesn't care about. I think those would expand the ecosystem, not fracture it.

[Kenny Lau]

But why would you want to default to creating an alternative rather than making mathlib4 better?

[Bulhwi Cha]

One could do both simultaneously, although it'd increase the amount of the work.

[Jeremy Ravenel]

When someone has done work in formalization, they have usually selected a topic for which they have a refined approach or improvement, so maybe they get irritated when the refinements aren't considered separately.

Sorry if this interrupts some from the topic here.

[Chris Hughes]

I think I've said most of what I wanted to say on this topic and I will switch off Zulip notifications and my engagement may be minimal from now on.

A lot has been written on these topics and any plan moving forward is probably best informed by that and not my particular case. Mathlib is more than just an open source project, it is also an academic research project and this brings different challenges, and different things have been written about good practice there. It may also play a role similar to that of an academic journal; people have talked about how getting something merged into mathlib may be a stamp of approval for a formalization paper. It is also the project that is dominating the field of formalized mathematics right now, so it's important to get it right.