New user, number theory PR in queue

Stream: new members

[Mathieu Gagne]

Hello!  My name is Mathieu Gagne and I just created my first (modest) pull request to Mathlib4 (#35573).  A little bit about me: after a PhD in Mathematics in 1997, I became a software engineer.  Now retired, math is back at the forefront of my interests.

I am interested in Number Theory.  I do not have a well defined plan viz. formalization, but am excited by the endeavor.  For practice I have been working through exercises and theorems in Apostol's ANT book, and this PR came up as an easy opportunity.  (Though the learning curve for formalization has been very steep!)

[Snir Broshi]

Hello! You might be interested in #PrimeNumberTheorem+, the "sibling theorem" to your theorem as you called it originated from there

[Mathieu Gagne]

Hello Snir, ah, that makes a lot of sense! Nice, the original PR. Things are moving so fast. And thank you for the welcome. I am aware of the PrimeNumberTheoremAnd effort but hadn't been following closely.

My motivation right now is understanding how various equivalent forms of the PNT related to one another, and I thought this may be an interesting angle to dig into Lean. It's possible to stay modest, as there are many "easy" equivalences, which is nice!