Is there a plan to offload Mathlib.Computability to Cslib?

Stream: mathlib4

[Ching-Tsun Chou]

In a discussion thread about how things should be named in automata theory, @Shreyas Srinivas made the following claim:

#CSLib > Automata @ 💬

Is it true? I would appreciate some clarifications. I've always had the impression that mathlib wants to be all-encompassing and theoretical computer science is surely part of mathematics.

CC: @Jeremy Avigad , @Mario Carneiro , @Johan Commelin , @Leonardo de Moura , @Patrick Massot

[Shreyas Srinivas]

Example : #mathlib4 > Labelled Transition Systems (LTS) @ 💬 And you might also want to scroll down that thread to the last messages.

[Shreyas Srinivas]

More concrete example : #computer science > Automata theory in Lean4 @ 💬

[Tanner Duve]

I feel certain parts of the computability folder could reasonably move to cslib, specifically things about automata. but concepts like recursive functions and degree theory sit firmly in mathematics imo (people that work in these areas are exclusively housed in mathematics departments from what I have seen). But agreed with @Shreyas Srinivas that the boundaries are fuzzy.

[Ching-Tsun Chou]

@Tanner Duve I would appreciate an articulation of the philosophical rationale behind this distinction. Note that automata theory was invented by mathematical logicians to answer questions in logic and computability. For example, consider the following seminal paper:
Rabin and Scott - Finite_Automata_and_Their_Decision_Problems.pdf

[Ching-Tsun Chou]

Or this one:
Büchi - On a decision method in restricted second order arithmetic.pdf

[Tanner Duve]

It's true that formal models of computation have their roots in logic and foundations. I more so meant one could sensibly argue for automata theory today as being a "CS topic", since it's used in things like model checking and verification, automata learning, etc. (and taught to CS undergrads) I don't as much see classical recursion theory or degree theory as CS since from what I understand this kind of work is primarily done by logic people in math departments. Just my two cents though. In any case, computability isn't really on or related to anything on the list of mathematical interests of the mathlib maintainers, which is something else to consider. I PR'd some basic stuff about Turing degrees that took a while to merge for this reason.

[Tanner Duve]

But I'm now realizing this discussion was already had and this post was made for the maintainers to clarify

[Chris Henson]

Please try to avoid tagging a long list of people that are likely very busy.

To address the question: to me, this is a practical issue of the effective scopes of the respective libraries, not history of the field. My thought process (as a CSLib maintainer) is that anything of a CS flavor and likely to always stay in a leaf of the Mathlib import graph could possibly, with agreement of both libraries, be considered to move downstream.

As to the specific case of automata mentioned in the title, my suggestion was essentially Kim's that is linked. In CSLib, add the desired implementation of automata, then see if the existing code in Mathlib can be ported. If so, it seems to meet the criteria I listed.

[Ching-Tsun Chou]

Personally I want to see a clear policy statement from the mathlib community about their vision of the scope and ambition of mathlib. That's why I copied my query to some leaders of the community.

Whether a theory is a leaf node in mathlib can change over time. Some time ago I saw the following talks on YouTube:
https://www.fields.utoronto.ca/talks/Fractal-Dimensions-and-Büchi-Automata
https://www.fields.utoronto.ca/talks/Definability-Reals-Büchi-Automata
If I were to formalize such theories and add them to mathlib, then automata theory would not be leaf nodes anymore, would they? Do you consider such theories "mathematics" or "computer science"? Furthermore, if some leaf theories are removed, other theories may become new leaves. Do you keep going?

[Chris Henson]

Yes, there is change over time and a bit of social convention. I also am using "leaf" loosely and in comparison to Mathlib as a whole, say at roughly a module/directory level.

[Ruben Van de Velde]

The main limit on the scope of mathlib is, practically speaking, the availability of maintainers who can review incoming material.

[Yaël Dillies]

Historically, theoretical computer science has been well supported in languages other than lean/libraries other than mathlib, and mathlib specifically built itself as a sort of reaction to that. As a consequence, we now have an imbalance of maintaining/reviewing capacity away from computer science and it therefore seems very reasonable to move some computability theory out of mathlib and into a library with more suited maintainers.

[Yaël Dillies]

Regarding your example about Büchi automata and definable reals: Bringing niche topics back to the central table of mathematics within the paper literature takes time, much more time than it takes to move content between two Lean libraries. I think this is a non-issue

[Ching-Tsun Chou]

Why do you think splitting into a separate library will improve the maintaining/reviewing capacity? Can't you recruit cslib reviewers to review mathlib PRs?

And do you consider cslib to be a staging area for mathlib, so that contents in the former will eventually make their way into the latter? Or they will go their separate ways?

Finally, what do you consider to be the central part of mathematics? Does logic belong to that central part? Should (say) proof theory be put in mathlib or cslib? I'd appreciate a clear specification of the demarcation.

[Shreyas Srinivas]

I understand that you want clarity, but I am afraid there is no clear cut answer, only a heuristic : If something is studied largely in a CS department, and its publication venues are CS venues, then it probably goes to CSLib. Same for math. Proof theory might go to either with a slight substantial bias towards CSLib

[Bjørn Kjos-Hanssen]

How about as a rule of thumb, if something is used in solving one of Hilbert's problems it should go in Mathlib. Therefore (because of the 10th problem) basic computability theory goes in Mathlib.

[Shreyas Srinivas]

The decision rests with maintainers but I don’t see this as a viable criterion. Far too much of modern CS theory came out of Hilbert’s problems. Maybe it’s just easier to ask mathlib maintainers in each individual instance, since mathlib is the upstream library.

[Kevin Buzzard]

Ching-Tsun Chou said:

Finally, what do you consider to be the central part of mathematics? Does logic belong to that central part? Should (say) proof theory be put in mathlib or cslib? I'd appreciate a clear specification of the demarcation.

This is a delicate question and different maintainers have different opinions. There is no clear specification of what is or isn't suitable for mathlib, and attempts to make one in the past have just resulted in the realisation that different maintainers can have very different ideas about the answer. There are around 30 maintainers with quite different backgrounds and interests, so although you've made it quite clear that you are looking for precise rules, in practice this seems to be difficult to achieve.

[Ching-Tsun Chou]

This ambiguity was precisely why I asked the question. But even leaving that question aside, no one has addressed my other questions:

Why do you think splitting into a separate library will improve the maintaining/reviewing capacity? Can't you recruit cslib reviewers to review mathlib PRs?

And do you consider cslib to be a staging area for mathlib, so that contents in the former will eventually make their way into the latter? Or they will go their separate ways?

[Kevin Buzzard]

I love your optimism, but if you think that there is just a way that the mathlib maintainers can just magically make reviewers appear out of nowhere and review all our PRs then please explain how to make this happen, because right now the fact is that we have 2000 open PRs with more appearing every day. Reality is far more difficult than your mental model of the problem.

[Shreyas Srinivas]

Ching-Tsun Chou said:

This ambiguity was precisely why I asked the question. But even leaving that question aside, no one has addressed my other questions:

Why do you think splitting into a separate library will improve the maintaining/reviewing capacity? Can't you recruit cslib reviewers to review mathlib PRs?

And do you consider cslib to be a staging area for mathlib, so that contents in the former will eventually make their way into the latter? Or they will go their separate ways?

CSLib exists among other things to serve the formalisation goals of CS teachers and researchers. To answer one of your questions: no it’s probably not going to serve as a staging area for mathlib. At least, no such intention has been expressed by the project steering committee or maintainers so far. CS works very differently from math.

[Ching-Tsun Chou]

Is there a website that tells us who are the project steering committee members and maintainers of cslib?

[Ching-Tsun Chou]

Namely, something like this: https://leanprover-community.github.io/teams.html

[Shreyas Srinivas]

As of now there is the google docs presentation from the initial meetings and the Zulip messages from some leaders on the CSLib channel. You are looking at a project in an extremely early stage.

[Ching-Tsun Chou]

I was in that meeting. In fact, I attended both occurrences. As far as I can recall, the only thing that happened was some Amazon people announced what they wanted to do, most of which don't seem to have appeared in https://github.com/leanprover/cslib yet. I don't recall there were any announcement of a steering committee or maintainers. If I have missed the announcements, please provide us with the URLs.

[Chris Henson]

I completely agree with Kevin, but will attempt to answer your questions as much as possible:

1) Of course splitting does not by default increase the number of reviewers, but it helps to have a designated area for CS-related work. I personally think this fills a need that has existed for a while, and hope it will relieve a (very small) bit of burden from Mathlib reviewers.

2) As I have mentioned previously, I have already made a couple of small PRs to Mathlib that originated in CSLib. The reverse has also happened, where a PR in Mathlib was determined to be a better fit for CSlib. In general though no, calling it a "staging area" for Mathlib is inaccurate. We are downstream and use certain infrastructure, but core results will remain in CSLib. While we have been discussing topics in a fuzzy area, there is certainly much work that is unambiguously CS and whose terminal destination is CSLib. There's an entire body of work about imperative verification not yet released publicly yet, as Shreyas said this is the project in an early state.

3) There is a description in the repo that lists the current steering committee/maintainers: https://github.com/leanprover/cslib/blob/main/GOVERNANCE.md

[Mario Carneiro]

Keeping in mind what Kevin said that there are disagreements among the maintainers and I am representing only my own opinion: cslib is not a mathlib initiative; it was not started by mathlib maintainers and it is not hosted under leanprover-community (despite my urging). The scope of cslib is up to the maintainers of cslib, and contributors are free to contribute material to cslib or mathlib as they please. At the moment, they clearly have a nonempty intersection of possible coverage areas, and this isn't likely to change anytime soon. It's best to just decide where to put stuff pragmatically based on where you will get the best reviews.

[Mario Carneiro]

Mathlib currently has no policy of moving things to cslib in any systematic fashion. Which is to say: the answer to the title question is no, there is no plan to move Mathlib.Computability to CSLib. Maybe you wanted to propose such a plan, but right now that plan does not exist. I would likely be against it for the time being, citing concerns about maintainership and the uncertain future of cslib.

[Chris Henson]

I suppose I should also clarify that these are my own opinions as a individual maintainer of this new project. As indicated in the maintainer list, I am primarily reviewing and working on lambda calculi formalizations and just happened to see this thread.

I will note regarding hosting that it is correct that we are not under leanprover-community, but we are under leanprover.

[Mario Carneiro]

indeed, and these are separate organizations (the FRO vs mathlib + MI)

[Mario Carneiro]

I think it would have been better to have cslib under the leanprover-community umbrella, but it was initiated by a group that seemed to have ties to Leo so I understand how it ended up in leanprover

[Mario Carneiro]

because of this (both the fact that mathlib and cslib maintainers have empty intersection AFAIK and that they are in separate umbrella orgs), transferring material from one repo to another is actually changing "owners", which complicates matters and makes it more than just moving things to another folder for topic coherence reasons

[Yaël Dillies]

Ching-Tsun Chou said:

Why do you think splitting into a separate library will improve the maintaining/reviewing capacity? Can't you recruit cslib reviewers to review mathlib PRs?

Reviewing mathlib PRs is hard and it is not clear to me that training cslib reviewers to do that job is any more efficient than just letting them run their own thing

[Shreyas Srinivas]

I want to point out that I was answering in the context of whether CSLib should assume some latitude in defining automata. I did not speak of any plan to move computability from mathlib, just that maintainers seem to lean in the direction (see examples provided). I am clarifying this since I am quoted in the message that started this whole thread. There is a mismatch between the title and the leading message.

[Kevin Buzzard]

PS @Ching-Tsun Chou I do think you are asking good and important questions, and I'm glad you're asking them. My answers are an attempt to demonstrate that in practice these questions are very complicated to answer. Questions such as "what is in scope for mathlib" have of course been asked several times before; it's just that all attempts to "officially" answer them have failed, basically because it is hard to get 30 people to agree on something.

[Ching-Tsun Chou]

Thanks to all who commented. It is good to know where everyone stands.

[Violeta Hernández]

I'm not a Mathlib maintainer, but my own view has always been that Mathlib should be cross-disciplinary. Not in the sense that every single discipline should be crammed into it, but rather that all the different disciplines within it should complement each other.

[Violeta Hernández]

Game theory was considered too niche to ever be used elsewhere, so it was split up (into yet another repository outside of the leanprover-community umbrella). Maybe computational theory fits that same description?

[Violeta Hernández]

:fire: maybe category theory fits that description too? I've seldom seen a non-category theory file importing a category theory one.

[Kenny Lau]

AG imports CT all the time

[Aaron Liu]

if the heuristic is "imported by another" then model theory is looking

[Violeta Hernández]

Do we have Ax-Grothendieck in Mathlib? (and if so, do we actually prove it via model theory?)

[Violeta Hernández]

I feel like a model theory project is something that could totally exist if there was more interest in it.

[Bryan Wang]

O-minimality in model theory has recently had some spectacular applications in arithmetic geometry (I think due to Jonathan Pila and collaborators), and I recall (learning from zulip in fact!) some recent work linking game theory and Harder-Narasimhan theory in algebraic geometry, which has in fact been formalized in Lean. And for computability theory, the resolution of Hilbert's tenth problem comes to mind.

[Bryan Wang]

My personal take is that while practical considerations should rightfully take precedence for now, I think we should still keep a view towards unity in the long run. Algebraic geometry in mathlib imports all sorts of things from RingTheory to Geometry to Topology to CategoryTheory, I can't imagine if the community had started out with separate libraries for all of those.

[Bryan Wang]

Violeta Hernández said:

Do we have Ax-Grothendieck in Mathlib? (and if so, do we actually prove it via model theory?)

I think there's FieldTheory.AxGrothendieck and I think it does use model theory (but I don't know the details)

[Michael Rothgang]

My understanding (not a maintainer, so no inside knowledge) is that moving combinatorial game theory to a separate repository already follows from practical considerations (no maintainers with the relevant expertise). If that changes and it is suddenly needed for other mathematics clearly in scope for mathlib, I wouldn't be surprised by it moving back.

[Bolton Bailey]

To propose an alternative: Is there some merit to the idea of copying the computability content from Mathlib without removing it, and simply not importing that part of the library. This would alleviate the issue of lots of Mathlib content disappearing all at once, and perhaps it would be possible due to the new module system. It might also allow us to make changes to the developments that make them better suited to other content in each library.

[Ruben Van de Velde]

Please don't :)

[Bolton Bailey]

I guess for some context, I have wanted to start putting some basic complexity theory into cslib (#CSLib > Complexity Theory in CSLib @ 💬 ), and I am currently wondering where I would put the theorem that a composition of polynomial time functions is itself polynomial time. On the one hand, this feels like this is starting to get into classic topics from undergrad CS and it really feels more appropriate for CSLib than Mathlib. On the other hand, it feels strange that this theorem would go in a different file, let alone a different repository, from the theorem that says that the identity function is polytime computable. What do people think would be the best way for me to proceed with this development?

[Mario Carneiro]

if it can be expressed using the computability library, feel free to PR it to mathlib

[Mario Carneiro]

if you want to commit it to cslib you can do that too. It's just a question of which maintainers you want to review it

[Kim Morrison]

You could also propose moving entire files from Mathlib to Cslib.

My understanding is that we don't currently have a good deprecation mechanism for moving individual declarations downstream (because you'd have to leave a deprecation message upstream, that would then cause a collision downstream), but we do have a good mechanism for deprecating entire files in a way that doesn't cause a problem downstream (and allows for including a message pointing to the downstream library).

I would love to have some suggestions for how to orchestrate moving individual declarations into downstream libraries, leaving appropriate deprecations for users.

[Bolton Bailey]

Well, it seems @Ruben Van de Velde thinks that we shouldn't duplicate code across repositories. I suppose I share concerns about that, such as the possibility that if the repositories have the same names for the same or similar concepts, then it will become difficult to simultaneously import both mathlib and cslib in further downstream repositories.

I think in the long term, it would be nice to validate the models of computation that CSLib will specify by proving that their notion of polynomial time is equivalent to the Turing machine notion, and so if I had my druthers I might say that docs#TM2ComputableInTime is about where I would start preferring content be moved. This is ~100 lines in a leaf file anyway, and I think it would be hard to find concepts downstream of this definition that are are not "CS" concepts.

[Mario Carneiro]

you can just put the things in different namespaces to avoid the name clash issues with duplication

[Mario Carneiro]

obviously duplication is tech debt and shouldn't be encouraged per se, but short term duplication is okay as a means to grease the wheels while something is going through review

[Snir Broshi]

Just to cross-link, in case not everyone here saw it: #mathlib4 > Move automata theory in mathlib to CSLib?

[Edward van de Meent]

i'd like to note my worry that if too much computability theory moves to CSlib, we maybe won't have the definitions in mathlib for computability/realizability topoi... I'm not knowledgeable about the exact definitions required for these (yet, maybe in a year or two) but i do suspect that this ought to be possible to have in mathlib...

[Edward van de Meent]

perhaps someone more knowledgeable on the topic can comment exactly what parts of computability theory are necessary for these?

[Mario Carneiro]

I think we shouldn't move anything out of mathlib computability ATM; everything which is there is already in scope and "being more CS than math" is not for me sufficient reason to not have it in mathlib

[Mario Carneiro]

this is kind of a branding issue caused by having a project called "cslib" which implies this is where the line should be drawn but I don't subscribe to it

[Snir Broshi]

Edward van de Meent said:

we maybe won't have the definitions in mathlib for computability/realizability topoi

Can Mathlib perhaps depend on CSLib? As long as there is no import cycle between the two, can two projects depend on each other?

[Mario Carneiro]

no that's not possible

[Snir Broshi]

Is it possible to make it possible?

[Mario Carneiro]

ask @Mac Malone

[Shreyas Srinivas]

CSLib ought to retain some latitude in including definitions for the same things as mathlib but which are more convenient in CS

[Shreyas Srinivas]

Although I agree that the very branding of CSLib as “the” computer science library is going to be a source of some trouble.

[Ruben Van de Velde]

I think more than "being more CS than math" the issue might be that there's quite low reviewer capacity for this part of mathlib

[Fabrizio Montesi]

Gone through the thread. A few comments for the sake of clarity:

• What I'm discussing in #mathlib4 > Move automata theory in mathlib to CSLib? is moving automata only for now. The reason is technical: the way we formulate automata in cslib depends (for good reasons) on things that (for good reasons) were deemed out of scope for mathlib and instead sit very nicely in cslib. I'd like to unify APIs/naming, prevent tech debt, and avoid people doing duplicated work as much as possible.

• The rest of computability in mathlib is another matter. Some parts maybe should never get out of mathlib, or at the very least require much more planning. I believe we should analyse each case carefully -- also, the situation might evolve over time.

[Chris Henson]

Shreyas Srinivas said:

Although I agree that the very branding of CSLib as “the” computer science library is going to be a source of some trouble.

I certain don't make the claim that all computer science has to happen in CSLib, just as all math does not have to happen in Mathlib. As an example, my involvement in CSLib started because I wanted to formalize categorical semantics, and along the way required lambda calculi. I think it is nice to have some of this in an "official" location, and in the nearish future I plan to provide tooling that will allow users downstream of CSLib to more easily make their own lambda calculi formalizaitons.

[Mac Malone]

Snir Broshi said:

Can Mathlib perhaps depend on CSLib? As long as there is no import cycle between the two, can two projects depend on each other?

This is something that could be supported in the future. It is very similar to the notion of a "peer" dependency in other package managers. If this is something CSLib decides it needs to do, that would be a good motivation to implement this. However, without such a motivater, this would not currently be a prioritized feature.

[Eric Wieser]

Ruben Van de Velde said:

I think more than "being more CS than math" the issue might be that there's quite low reviewer capacity for this part of mathlib

Maybe it's worth emphasizing that it is totally reasonable (and encouraged) for cslib contributors to review mathlib PRs; mathlib maintainers and reviewers are not the only people capable of leaving feedback, and if we see approval from a subject expert then that gets things very close to a merge

[Eric Wieser]

(of course we can't expect cslib contributors to watch the PR list, but if a cslib PR depends on a mathlib one they you shouldn't feel powerless to help it move along)

[Fabrizio Montesi]

Fully agreed, and I've seen people doing that already.

It doesn't help the case of automata much, unfortunately (which is the topic of the thread I opened), because it's not a case of 'we're missing features from mathlib' (which we already have a way to deal with).

[Mario Carneiro]

which thread?

[Fabrizio Montesi]

The one linked here https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20there.20a.20plan.20to.20offload.20Mathlib.2EComputability.20to.20Cslib.3F/near/563480796

(The mobile interface is giving me some trouble with copying the link directly, sorry.)

[Ching-Tsun Chou]

I wonder if it is possible to carve out a subtree of mathlib to become cslib, which will be controlled by the current CSLib personnels. Here by "control" I mean the decisions of what code gets into that subtree. Then there is no issue of whether mathlib and cslib can refer to each other and solves the "who can review the code?" problem.

[Mario Carneiro]

I have been in support for a while now of having domain-specific maintainers as a means of getting mathlib past its current organizational bottleneck. I think what you are proposing is certainly possible, but I would phrase it more as cslib maintainers becoming mathlib maintainers specializing for that subfolder

[Mario Carneiro]

there is nothing stopping people from having multiple hats

[Fabrizio Montesi]

Nobody disagrees with that but it doesn't solve the problem that we'd like to use some of cslib's APIs in the design of automata theory (and more).
Cslib is also gonna be a more natural place to have probabilistic and weighted automata and the like, because they are instances of the respective transition system generalisations (which we'd certainly develop once we get to this kind of machines).
More of such examples will likely pop up.

[Mario Carneiro]

I think if people were on board with the general plan it wouldn't be that hard to get cslib maintainers to first review a lot of cs-related mathlib PRs and then graduate to being a full mathlib maintainer. The mathlib maintainer team has long recognized that we lack expertise and review bandwidth for cs topics so I think that would work out well

[Mario Carneiro]

@Fabrizio Montesi You might need to be more specific about that, but I think the answer is that you should either upstream this "cslib API" to mathlib or else create a compatible API which cslib can build on

[Fabrizio Montesi]

That has been discussed at length and LTS were deemed out of scope.

[Mario Carneiro]

okay so leave LTS out of it

[Fabrizio Montesi]

Our def of NFA extends LTS. :⁠-⁠)

[Mario Carneiro]

Eh, that sounds like a reason to have them in mathlib

[Mario Carneiro]

maybe not the full theory but the bare definition

[Fabrizio Montesi]

A big chunk of the theory is necessary to prove stuff about nfa elegantly

[Fabrizio Montesi]

(but not necessary to do it in general, ofc)

[Mario Carneiro]

then that's also a reason for inclusion for that

[Mario Carneiro]

like, if you need it to do something in mathlib then that on its own is a cogent justification for inclusion in mathlib

[Fabrizio Montesi]

That's a possible viewpoint, ofc. The other is that automata could just be in cslib.
I'm fine either way. I was the one originally proposing LTS for mathlib, but there was no interest.

But why is it so important to have automata in mathlib?

[Mario Carneiro]

The point is that we need people, not definitions and proofs

[Mario Carneiro]

I am personally of the opinion that all theoretical CS is in scope of mathlib, but we need more people to join the review and maintainer teams

[Mario Carneiro]

having a separate library is and always was a backup plan for the case where the review capacity doesn't appear in time for your personal roadmap

[Mario Carneiro]

There are other mathlib maintainers that will of course disagree with me, but they are not subject matter experts on this material. That's why we need more subgroupings of mathlib with their own smaller teams.

[Shreyas Srinivas]

I agree with Mario but I don’t know how mathlib maintainers are recruited for an area that doesn’t exist in mathlib yet.

[Mario Carneiro]

the folder already exists

[Mario Carneiro]

that's the whole reason we're having this discussion

[Mario Carneiro]

if it was a completely disjoint topic split I don't think it would be an issue

[Mario Carneiro]

but that almost never happens in mathlib, it's very interconnected and even if there are currently no or almost no connections you can find a few people who have ideas and/or plans which would use area X to contribute to area Y

[Shreyas Srinivas]

I mean the content in computability is not substantial compared to what CSLib is aiming for. Also the name is computability which is already limited in scope.

[Kevin Buzzard]

Fabrizio Montesi said:

But why is it so important to have automata in mathlib?

Mathematicians prove theorems about automatic groups (for example all mapping class groups of surfaces are automatic) and I would very much hope to be able to state those theorems going forwards, but the definition which I know of automatic groups needs e.g. regular languages and finite state automata. However it would be fine just to have basic definitions in mathlib as far as I'm concerned.

[Fabrizio Montesi]

For the record, I think alike on lots of things you wrote, Mario. (And when it was pointed out for LTS that mathlib didn't have good reviewers for that, I offered myself.)
In general, one could have this discussion for many of the things currently or soon to be in the 'Foundations' and 'Languages' directories of cslib.

It's not just one directory though, unless you mean that LTS and their equivalences (like bisimilarity) should live under 'Computability'. We'd need to open up mathlib to semantics, maybe more..
So it's more of an area(s) maintainership issue. Also, we'd have to discuss the opposite concern (moving things out of cslib's maintainership).

[Fabrizio Montesi]

Kevin Buzzard said:

Fabrizio Montesi said:

But why is it so important to have automata in mathlib?

Mathematicians prove theorems about automatic groups (for example all mapping class groups of surfaces are automatic) and I would very much hope to be able to state those theorems going forwards, but the definition which I know of automatic groups needs e.g. regular languages and finite state automata. However it would be fine just to have basic definitions in mathlib as far as I'm concerned.

Thanks for this point, that's important to consider. (Side note: This makes me think even more that we might want a peer dependency in the future... :⁠-⁠))

[Mario Carneiro]

Fabrizio Montesi said:

It's not just one directory though, unless you mean that LTS and their equivalences (like bisimilarity) should live under 'Computability'.

If the material needs to be split into multiple directories, that's fine, that's up to the maintainers of the material and isn't really a big deal one way or another

[Chris Henson]

Mario Carneiro said:

I am personally of the opinion that all theoretical CS is in scope of mathlib, but we need more people to join the review and maintainer teams

How widely held is this view? My impression is that if I had tried to contribute say my work on lambda calculi, especially given we want multiple type systems and styles of binding, it would have been likely to stall early.

To me the discussions of moving things like LTS to Mathlib is the mirror of concerns with downstreaming. The concept is new to me, but I think @Mac Malone's idea of a peer dependency could go a long ways to resolve some of these problems.

[Mario Carneiro]

proving the equivalence of lambda calculus and turing machines was definitely on my roadmap for the computability library, although I ran out of steam to push it myself

[Mario Carneiro]

lambda calculus is also promising as a target for lean translation for an automatic computability prover for arbitrary functions

[Kim Morrison]

I would much rather see that we move things from Mathlib to Cslib where possible. Currently Mathlib has a large maintainer team, and membership of this group means many different things: both ability to use bors merge, but also full participation in our consensus-falling-back-to-voting mechanism for decision making. This makes it hard, and slow, to add more maintainers. For areas that are not growing particularly actively in Mathlib (and I think NFAs, and indeed all of Mathlib.Computability, is included in this), and are constrained by lack of availability of reviewers or maintainers at Mathlib, I would strongly encourage moving them to downstream libraries, in cases where there is sufficient activity/interest/momentum/infrastructure (and I think Cslib by now clearly meets that bar).

[Mario Carneiro]

Well, that's exactly why I've been arguing for mathlib maintenance to hierarchize some more, with smaller fiefdoms controlled by smaller subgroups of the maintainers so that we don't need one flat decision-making apparatus for everything. That's really an internal problem and I don't see why we can't grow maintainer membership 5x once we fix that

[Mario Carneiro]

Kim Morrison said:

This makes it hard, and slow, to add more maintainers. For areas that are not growing particularly actively in Mathlib (and I think NFAs, and indeed all of Mathlib.Computability, is included in this), and are constrained by lack of availability of reviewers or maintainers at Mathlib,

This sounds like an argument for just not growing mathlib beyond its current size, since bigger mathlib means more reviewers and maintainers and you are arguing against that. I don't think anyone wants that, and I seem to recall an Institute being created in the recent past to do the opposite

[Mario Carneiro]

so I think we need to solve our governance issues one way or another, and once we do I want us to crank up the membership to keep up with contributions (not just numerically but also representing the topic areas that our community is working on)

[Mario Carneiro]

and I think it's clear that CS is currently underrepresented and I don't want us to solve that by just kicking CS out of mathlib because it's not a clean split

[Mario Carneiro]

and also because I never stopped believing in the monorepo ideal of cross-discipline global coherence

[Kim Morrison]

My view is that this is actually the opposite of what you've been arguing! Let's take this to DMs, and see if we can resolve this there rather than having a public discussion about it based on misunderstandings.

[Violeta Hernández]

My perhaps biased opinion is that having these separate repositories for niche topics is a benefit to everyone. It means these projects won't get brought to a snail's pace by lack of available Mathlib maintainers, and it gives them more flexibility to try out radical stuff as their design coalesces.

[Violeta Hernández]

The CGT repo was birthed from a proposed refactor that would have totaled some 3,000 lines of diff had it been PR'd to Mathlib. Instead we split off, moved fast and broke stuff, and now the repository is thriving.

[Violeta Hernández]

I'm not against CGT eventually getting swallowed back into Mathlib, but I do think that without the opportunity to use this separate repository as a sort of staging ground, we would not have been able to develop the theory as far as we did. Perhaps CsLib could act in a similar way?

[Mario Carneiro]

certainly, cslib can function as a staging ground for mathlib in the same way that mathlib is a staging ground for batteries and batteries is a staging ground for lean core

[Mario Carneiro]

You can say the same about project repos like FLT, which accumulate things to upstream asynchronously

[Chris Henson]

Violeta Hernández said:

I'm not against CGT eventually getting swallowed back into Mathlib, but I do think that without the opportunity to use this separate repository as a sort of staging ground, we would not have been able to develop the theory as far as we did. Perhaps CsLib could act in a similar way?

This has been true of CSLib as well. I don't think for instance I would have pushed as far experimenting with grind and metaprogramming without a separate repo. A distinction I would make though is that I don't think CSLib will converge to something that makes sense to move into Mathlib.

We are grateful for the foundation that Mathlib provides, and we have already made some small PRs for upstreaming things that unambiguously belong in Mathlib. My main point is that, given the current practicalities of bootstrapping Mathlib reviewers/maintainers that Kim describes above and what seems to be the more prevailing opinion of the scope of Mathlib, there are distinct advantages for certain CS-oriented topics to move to CSLib. Especially if we are able to eventually have mutual dependency as Mac suggests, I think we can mostly satisfy everyone.

Again, I am not personally in a rush for this, and am very willing to work with Mathlib maintainers in whatever capacity is necessary to address any concerns.

[Mario Carneiro]

I think the main priority should be ensuring that any duplications are short lived and resolving any inconsistencies, so that the two libraries can be used together seamlessly

[Mario Carneiro]

deciding where individual items go is less important