Improve project ideas page

[reiniscirpons]

This PR improves the libsemigroups GSoC project page by enhancing the project descriptions and decorating them with some estimates of difficulty as well as proposed mentors. A preview of the new version is available at:

https://reinisc.id.lv/libsemigroups.github.io/gsoc/

@Joseph-Edwards @hivert @james-d-mitchell @flsmith @mtorpey : I have assigned each of you as a mentor on some of the projects listed here. Would you mind double checking and letting me know if there is any issue in the assignment or some other project you would also like to mentor?

[Joseph-Edwards]

This looks really good to me!

I've made a few typographic suggestions, and have a few comments related to the projects I have been assigned to:

Julia bindings Semigroups.jl for libsemigroups

I'm not sure if my understanding of Julia is sufficient to be a good mentor. If my role consisted of general chats about the bindings to help inform how the bindings are implemented, and otherwise supporting @james-d-mitchell, then I'm happy. If, however, my role would involve code reviews of Julia code (or other Julia specific things), I think I might be a bit out of my depth.

Formal verification of Knuth-Bendix and Todd-Coxeter

Very happy to be involved in this one. I'd need to brush up on my rocq, but overall I'm happy.

Improving errors and their messages in GAP

Very happy to be involved in this one. I don't have a super in depth knowledge of how GAP handles errors, but I don't think that should be a barrier (and it would hopefully be quite quick to learn).

Morphocompletion for Knuth-Bendix

Very happy to be involved in this one and, with a bit more information about the structure of the desired implemention, I am happy to be the sole mentor.

[reiniscirpons]

Merci for the suggestions Joe, incorporated now. With respect to the projects:

Julia bindings Semigroups.jl for libsemigroups
If my role consisted of general chats about the bindings to help inform how the bindings are implemented, and otherwise supporting @james-d-mitchell, then I'm happy.

Yes, me and James were thinking you would be a good fit because of your knowledge of the design decisions that went into the Python bindings, and the idea was to have this be a co-mentorship. It is also true that we would be looking for a candidate with a good knowledge of Julia already and mentoring would not necessarily mean that you need to be the one reviewing the PRs, which could be done by James for example.

Formal verification of Knuth-Bendix and Todd-Coxeter
I'd need to brush up on my rocq, but overall I'm happy.

Excellent! Overall the main idea would be to implement the logged rewriting (i.e. producing a Tietze transformation sequence during a run of Knuth-Bendix) which is fairly agnostic to Rocq or Lean. If the student is keen then we could also work a bit on turning this sequence into a Rocq proof, but this would not require much Rocq programming in the Knuth-Bendix case and either Florent or myself could provide mentorship with that.

Morphocompletion for Knuth-Bendix
Very happy to be involved in this one and, with a bit more information about the structure of the desired implemention, I am happy to be the sole mentor.

Glad to hear it. A very basic idea we had was something along the lines of:

1. Run Knuth-Bendix for X amount of time,
2. If it did not terminate, find the Y most common non-singleton subwords in all the relation words of the incomplete rewriting system,
3. Replace each of there relation words w by a new generator a and add a relation w = a,
4. Reinitialize the Knuth-Bendix object using the incomplete RWS + new generator relations and go to step 1.

This seems to be roughly the idea of the morphocompletion article linked in the project description. The idea would be for the student to implement a wrapper function or class around this in either C++ or Python and then to figure out good parameters. For example instead of running it for "X amount of time" we could do "X number of steps" or "X new relations added". And then tweaking how many subwords Y to add relations to as well as changing the notion of "most common" used (e.g. maybe we additionally prioritize longer or shorter substitutions) etc. Happy to meet and talk about this later on!

It is also true that we will only need to do this if our application to GSoC is successful, and then we will separately have students apply for some of these projects and not every project may be taken.

Thanks again for the suggestions Joe and for volunteering to mentor!

[james-d-mitchell]

Looks good, I suggest merging we can adjust mentors later if necessary