Weighted Formal Languages

Stream: mathlib4

[Rudy Peterson]

Hello everyone,

My name is Rudy, and I am interested in mechanizing the theory of weighted formal languages for Mathlib4.

I see there already extensive libraries in the Computability part of Mathlib4 for regular languages and context free grammars, but maybe there's space for weighted languages as well? I would like to primarily consider semiring weighted finite state automata. I am also interested in proving closure properties and transformations for unweighted languages. I am also considering formalizing tree automata.

Is anybody already working on this? I'd be interested in collaborating if people are already developing these libraries.

Thanks!
Rudy

[Patrick Massot]

It would very probably be hard to find maintainer reviewing this. I think you will be a lot less frustrated if you create a library depending on Mathlib.

[Ruben Van de Velde]

That's not to say you can't ask for help or look for collaborators here, btw. We're always happy to see people formalizing their interests, but getting things into mathlib if none of the maintainers has expertise is an exercise in frustration, unfortunately

[Harald Husum]

Ruben Van de Velde said:

That's not to say you can't ask for help or look for collaborators here, btw. We're always happy to see people formalizing their interests, but getting things into mathlib if none of the maintainers has expertise is an exercise in frustration, unfortunately

Just out of curiosity, how does one go about bootstrapping a not previously covered area of mathematics im marthlib? Since one needs one maintainer to have expertise, I'm assuming one would then aim to become that maintainer. But you can't really self-review your own PRs anyway, so you'd then need to get a grad student to do the coding for you? That is, if only one maintainer is an expert in a certain field, they can't really contribute their expertise to mathlib.

This isn't a critique: I'm not an active contributor to mathlib and have not experienced the potential frustration mentioned here. I'm just wondering whether there has been put much thought into how to go about these things.

[Ruben Van de Velde]

I guess you could find at least two persons to start contributing on other subjects and work their way into the maintainers team :)

[Martin Dvořák]

I am not a maintainer and I cannot speak for them; however, I will be happy to review PRs about weighted formal languages.

[Kim Morrison]

Yes, we have thought about this some, and acknowledge that it is a difficult problem. My suggestion is to start (ideally with other people interested in adjacent topics --- but it will take a leader!) a repository down stream of Mathlib. You are very welcome to use this zulip to discuss PRs to it (as well as organizational issues). I think people here will be very happy to help set up the repo, including showing you how to set up good CI, and how to turn on all the Mathlib linters so you get automatic code review based on those.

[Kim Morrison]

There are some in progress tools for automatically bumping the Mathlib dependency of downstream projects, and we would really like to keep working on these tools and make them even better.

[Kim Morrison]

If/when there's reason to believe the project has a viable critical mass of contributors, we're happy to host it on the leanprover-community GitHub organization if that is preferred.