Intro: Niels Voss

Stream: new members

[Niels Voss]

Hi! My name is Niels Voss. I am an 11th grader in high school and I started learning Lean this summer. I have already asked a few questions in this Zulip chat and have read through “Theorem Proving in Lean” for Lean 3. I also am working on a PR about Fermat pseudoprimes.

I know some elementary number theory, but don’t really have any experience in other branches of higher mathematics. In particular, the semiring and ring typeclasses in mathlib are my first real exposure to abstract algebra. I also seem to have a bit of trouble making my proofs short and readable, but I think that’s something I’ll get better with over time.

[Kevin Buzzard]

If you make PRs then people will read and help you with your code, although right now we're in a bit of a weird situation, with many people busy porting mathlib from Lean 3 to Lean 4.

[Niels Voss]

I do actually have an open Pull Request (#17632) but I kind of realized that the migration would complicate things. I'm not particularly worried if it takes a long time to get reviewed, since I can write code for other topics to get more practice. There was a Zulip thread about it a while ago but it didn't really get resolved.

[Kevin Buzzard]

Oh yeah I remember that discussion! You seemed to be OK in the end because you were only subtracting 1 from things which you knew were >= 1 and so you wouldn't run into pathologies.

[Kevin Buzzard]

It's a great shame that you're so young and your PR was basically ignored; most reviewers are now actively working on the port, and so the list of mathlib3 PRs just keeps growing and growing and I'm not entirely sure what will happen to it. To a lot of people's eyes right now your work will be seen as low priority because it's not actively helping with the port (in fact in some sense it's actively hindering it, because it just means that there's more to port).

[Niels Voss]

I'm planning on working with Dirichlet inverses (as far as I know, mathlib only has code on Dirichlet convolutions, not inverses), which will hopefully be less algebra heavy than Fermat pseudoprimes. As far as the current PR goes, I think I'll just wait until a later stage in the migration to figure out what will happen to it, since I probably won't be able to do much work over the holidays anyways.

[Martin Dvořák]

You did a lot of work! Congratulations!

Unfortunately, I was able to leave only superficial comments about your code.