Rodrigo C

Stream: new members

[Rodrigo C]

Hello everyone!

I'm Rodrigo. I am currently an ML/AI engineer working in tech but have always been fascinated by math. Officially, I studied CS for undergrad and master's with a minor in math.

I've recently become intrigued by potentially contributing to math research myself, especially when I heard Terence Tao mentioning that there have been some polymath projects benefiting from contributions from non-experts. I'd especially be curious if there is any way to leverage my strengths in SWE, etc. to push formalization of math forward. Making useful contributions to pure math has always seemed very out of reach for me, but maybe this could be a unique opportunity :D

Any recommendations and advice would be really appreciated! In general I think I'd be more likely to be helpful for topics that don't require very deep background (for example some areas of probability, combinatorics, especially topics relevant to ML/statistics/CS). I think my ideal project would involve contributing to some low-hanging fruit areas that are fundamental to recent research, but just have not really been done yet. Would love to hear if anyone has specific open starter projects on these topics or anything else that you think might be a good fit!

Also would be interested if there are infrastructure / tooling projects that could greatly improve quality of life for contributors, since this might be more up my alley strengths-wise (but I would really like to contribute to the formalization itself of course).

[Michael Rothgang]

Welcome! There is lots of infrastructure underpinning mathlib (and even a hot off the press paper about it), and all of that can use some help. Particularly by someone who knows more CS than a mathematician-who-had-CS-as-a-hobby-of-sorts (like me).

[Michael Rothgang]

Some ideas that come to my mind

• helping with syntax linters: typically, you'd be programming something in Lean. (In involves metaprogramming, but relatively light one.) There's a wishlist issue on github, but I can also suggest projects directly.
• one example, relatively easy: lint for non-existent filenames in documentation strings #mathlib4 > Linter for links?. Not hard by any means, but useful.
• if you like heavy metaprogramming: there are a lot of ideas on better tactics, so tactic writing could be a fun project. (My advice, though: pair, or talk often enough, with somebody who has a clear idea what the tactic should do. This may influence your implementation choices.) There's a zulip thread with tactic ideas.
• a linter to generalise theorems: there was been prior work on this, see #mathlib4 > linter to generalize theorems (and coordinate with the student there who's also interested)
• a tool to suggest a good name for your declaration (see also the above thread)

[Michael Rothgang]

There's one more project which can use lots of help: mathlib's review dashboard https://leanprover-community.github.io/queueboard/. This is used by many reviewers, so possibly higher-impact than the others. The project is well-documented, even has a list of "good first issues" (well, still one and a half - I could write instructions for more).

[Michael Rothgang]

If you like backend/continuous integration work (or just a solid CS problem), there's also a bunch of other tasks that need doing (that aren't documented, among others because they depend on context which takes a moment to write down). If you're interested, we could certainly discuss.

[Michael Rothgang]

You're of course equally welcome to work on formalisation of things --- but my point is: we also need you if you're more of a programmer; mathlib survives because of its infrastructure, and that can always use more help!

[Rodrigo C]

Awesome! Thanks for the ideas. I think for just a starter project, this one "* one example, relatively easy: lint for non-existent filenames in documentation strings #mathlib4 > Linter for links?. Not hard by any means, but useful." sounds the most approachable and can get me to start grokking Lean and the mathlib codebase.

Perhaps I can start branching out from there.

[Damiano Testa]

In case it helps, #mathlib4 > Naming convention: succ vs. add_one @ 💬 is a recent example of some code that loops through all the declarations in the environment. You can extract the docstring of a declaration (if it has one) using docs#Lean.findDocString?.