Code/annotation standards and maintainability

Stream: PrimeNumberTheorem+

[(Tom de Groot) Tomodovodoo]

There's currently an interesting conversation about formatting standards (in the context of AI generated proofs) in #733, and currently I feel like there isn't a consensus inside the current codebase on how code must be commented and formatted.

As I partially described in the last PR comments, maybe we should take the opportunity to define such a code and annotation formatting standard? As in, do we leave comments on smaller lemmas, keep them uncommented, do we leave white spaces between local lemmas (have:), should we annotate them with a single liner, etc. Especially at a time where I, and many other newlings are coming to this project from the current hyper around auto formalization tools, a strong standard can keep the backlog clean and can create stricter PR rules.

I feel like in this manner, we can create a more maintainable codebase and a more maintainable PR list, especially when over time parts of our code might get merged in mathlib in some capacity, and we can reduce refactoring time in the future.

What do you guys think? Keep it quite loose as it is right now, or enforce some stricter rules?

[Kim Morrison]

An opinionated code formatter is in the works this quarter. My advice is to not worry too much right now, and then blindly obey the formatter when it is ready.