Looking for areas to contribute

Stream: new members

[David Wegmann]

Hello Lean people,

I recently finished my master's degree and have a lot of time at the moment. I did a lot of personal Lean 4/Coq/Agda projects that I enjoyed during my time at university. I feel very comfortable using Lean 4, but I never contributed to mathlib or some other official Lean repo.

Are there any areas of mathlib or the rest of the lean ecosystem that might welcome a contribution from a newcomer?

My areas of interest:

• Theoretical CS
  • Lambda calculus, type theory (my bachelor's thesis was formalizing System F omega in Coq)
  • track B theoretical cs category theory stuff
  • Basic complexity theory (I don't know the deep lore of niche complexity classes though)
• Math
  • Standard undergraduate topics (algebra, analysis, topology, etc.)
  • Category theory
    • Monoidal categories, tensor categories
    • Categorical homotopy theory
    • Abelian categories (in context of homological algebra)
  • Algebraic topology
  • Differential geometry
• Machine learning
  • I can use PyTorch
  • To understand the inner workings of PyTorch, I wrote my own autograd library in Lean 4 that uses the dependent types to eliminate errors when strining together the architecture.

I would also be interested in contributing to any related areas of the topics on this list or anything else.

[Yongxi Lin (Aaron)]

For example, you can claim issues in https://github.com/google-deepmind/formal-conjectures and https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

[Yongxi Lin (Aaron)]

and you can also check out issues of Mathlib: https://github.com/leanprover-community/mathlib4/issues

[Chris Henson]

In #CSLib we have lambda calculi with locally nameless binding for STLC and System F with subtyping. We have progress/preservation for both and confluence for simple types, but strong normalization would be a welcome contribution that doesn't require adding too many new definitions.

(In the future we plan to have well scoped indices in the style of Autosubst2, but I don't think any of this is great for a first contribution)

[David Wegmann]

I did actually do strong norm as my bachelos thesis :), porting that should be straight forward. haven't done locally nameless, purely debrujin, but I think I can brush up on that.

[David Wegmann]

@Chris Henson is there a seperate cslib zulip?

[Chris Henson]

There is a channel in this Zulip that my above message links to.

Here is where the locally nameless development is. Feel free to post in the CSLib channel if you have questions.

[Chris Henson]

The module docstring at the top of each file also lists a couple of references

[David Wegmann]

Thank you. I'll download the library and play around with Lambda Calculus a bit, if I feel comfortable implementing strong norm I'll get back to you in the CSLib Channel.