New user, trying to fit

Stream: new members

[Ralf Stephan]

After doing my first classical number theory proofs, having read that Mathlib PRs are needed only for modern additions. OTOH, I've read about the attempt to build a system that wins the Olympiad, where old number theory would have possibly more use? But these systems would likely be closed/proprietary, and the only way to contribute there would be to put lean files on GitHub and hope they will be scraped by someone. So, my question:

Regarding proofs for things like "$a^{2m+1}+1$ can be divided by $a+1$" [Euler, E026] or "if any numbers of the form $a^n+1$ are prime, it is necessary, that they be of the form $a^{2^m}+1$" [Euler, E026]

• are these of ANY use?
• is someone collecting classical NT lean files?
• is there a repo dedicated to the Olympiad effort?
• is there a repo taking contributions that don't go in Mathlib?

I would continue to improve my formalization skills but the answers to the above would change the path I'll take.

Thanks,

[Alex J. Best]

I think its quite nice to have some of these classical number theory things in mathlib. We don't only want things that are modern if older things are still relevant to mathematics that people do today. Certainly some of the work of Euler would be a welcome addition in many cases. The main thing to look for is that the results should be sufficiently general.

[Ralf Stephan]

Thanks, I should add here the link that was posted elsewhere: https://reservoir.lean-lang.org/