Formalising the Euler-Maclaurin formula

Stream: new members

[Kevin Barreto]

Hi all, I am new here. I am an undergraduate mathematics student at the University of Cambridge, and trying to become familiar with Lean 4.
I am looking to formalise more machinery for some of my work in analytic number theory, and a key ingredient, namely the Euler-Maclaurin formula, does not appear to be in Mathlib4. All the machinery to formally prove it seems to already exist, so I was wondering if this would be a good project to work on and contribute to Mathlib4?
It would also provide a short, immediate proof of Faulhaber's formula sum_range_pow as a corollary.

[Weiyi Wang]

It does sound like a good project! As in, it looks like something I would want to do as someone who has used Lean for less than a year

[Weiyi Wang]

Oh I see you were already tagged in the other discussion thread