attribution

Stream: condensed mathematics

[Johan Commelin]

Does anybody have an idea how to increase the balance in attribution for this project? In all the media attention only a few people are named. It's very sad, but I'm afraid we can't change what the journalists write.

One idea that might help a bit, is if there is a nice landing page that lists the team that worked on LTE. It this is only one click away, then maybe more people will see it. Currently, the only public listing is probably in Peter's second blogpost, and somewhere in a statistics page on github.

[Mario Carneiro]

actually I'm writing something that cites LTE now, and I would like a list. What did you post on quanta?

[Johan Commelin]

The team involved in this project consisted of: Patrick Massot, Adam
Topaz, Riccardo Brasca, Kevin Buzzard, Bhavik Mehta, Scott Morrison,
Damiano Testa, Heather Macbeth, Filippo A.E. Nuccio, and lots of help
from many other people in the Lean community!

[Mario Carneiro]

I guess you and Peter Scholze should also be mentioned?

[Johan Commelin]

But I'm open to changing that list. The good old "write a paper, list the authors alphabetically" is so much easier. But that doesn't really work with all the media stuff.

[Johan Commelin]

Mario Carneiro said:

I guess you and Peter Scholze should also be mentioned?

Right, but in the quanta article we both got mentioned quite a bit.

[Johan Commelin]

Also, people like you, and Reid, and Alex, also made some contributions. I don't know where to draw the line.

[Johan Commelin]

It's probably high time that we just have an open discussion about this.

[Mario Carneiro]

True. Was Clausen involved in the formalization at all? I don't recall him dropping by here but I might have missed something

[Matthew Ballard]

Do you have a press kit or press resources for the project?

[Johan Commelin]

Mario Carneiro said:

True. Was Clausen involved in the formalization at all? I don't recall him dropping by here but I might have missed something

Nope, he wasn't. As far as I know, this part of the proof is due to Scholze. But I think Clausen read through it at some point before LTE started.

[Johan Commelin]

Matthew Ballard said:

Do you have a press kit or press resources for the project?

Nope, I'm really a novice when it comes to these things.

[Matthew Ballard]

I am not really any better. (How many mathematicians need to manage the press?) But I imagine having a simple document easily digestible and easily available will help with attribution issues.

[Johan Commelin]

Johan Commelin said:

It's probably high time that we just have an open discussion about this.

If we ever write up an article in a non-mathematical venue (some big CS thing, maybe even Nature?) we'll have to play their game. And then listing the authors alphabetically isn't the custom. As far as I understand, first, second, and last author matter quite a bit.
If people have some good ideas about how to make decisions here, please share them.

[Johan Commelin]

Matthew Ballard said:

I am not really any better. (How many mathematicians need to manage the press?) But I imagine having a simple document easily digestible and easily available will help with attribution issues.

Agreed. But this also means that we need to agree on who is in the document, and where, and in which order. I don't feel like I can make such decisions in a good way. I think it's something we should do as a team/community.

[Adam Topaz]

Johan Commelin said:

One idea that might help a bit, is if there is a nice landing page that lists the team that worked on LTE. It this is only one click away, then maybe more people will see it. Currently, the only public listing is probably in Peter's second blogpost, and somewhere in a statistics page on github.

One (probably bad) approximation to such a list is under the following link?
https://github.com/leanprover-community/lean-liquid/contributors

[Johan Commelin]

Exactly, that's the statistics page on github that I was referring to

[Matthew Ballard]

Johan Commelin said:

Agreed. But this also means that we need to agree on who is in the document, and where, and in which order. I don't feel like I can make such decisions in a good way. I think it's something we should do as a team/community.

I have nothing useful to contribute to this point. Just wanted to point out the (perhaps obvious) general tendency of people is to default to the provided info.

[Riccardo Brasca]

The problem with that page is that it doesn't take into account contributions made directly in mathlib. For example Scott did a monumental work on chain complexes

[Adam Topaz]

I completely agree.

[Filippo A. E. Nuccio]

Johan Commelin said:

Johan Commelin said:

It's probably high time that we just have an open discussion about this.

If we ever write up an article in a non-mathematical venue (some big CS thing, maybe even Nature?) we'll have to play their game. And then listing the authors alphabetically isn't the custom. As far as I understand, first, second, and last author matter quite a bit.
If people have some good ideas about how to make decisions here, please share them.

Well, I think that you are addressing two problems at once, here. One is to understand who is in the set of contributing authors, which looks very hard to me; the second is to order it, which will be an easy matter (I guess easily and quickly agreed by all members).

[Adam Topaz]

authors : set People

[Adam Topaz]

Does it really make sense to figure out this stuff now, given that the project is still ongoing?

[Mario Carneiro]

I expect that the proof of theorem 9.4 is already a big multi-author publication waiting to happen

[Mario Carneiro]

no harm in getting a second paper out of it later

[Kevin Buzzard]

The instinct of the mathematician is to wait until it's all done and then to write a 50 page paper, not publish incrementally with short papers as is the preference in CS

[Eric Wieser]

One approach that could be taken is the one that SciPy took; a short list of sorted-by-contribution main authors, and an appendix of alphabetical small contributors.

[Adam Topaz]

"short" in this case is 34?