Is there any formalization, in any proof checking environment (Lean, Isabelle, etc.) of basic analytic number theory, say everything in a book like the Titchmarsh book (The Theory of the Riemann Zeta Function) or the Ingham book (The Distribution of Prime Numbers), or any equivalents?
6
-
$\begingroup$ A number of theorem provers have the prime number theorem. See cs.ru.nl/~freek/100 $\endgroup$– Jason RuteCommented Feb 20, 2023 at 18:25
-
$\begingroup$ Also it appears the Archive of Formal Proofs in Isabelle/HOL has some of this stuff. See isa-afp.org/entries/Zeta_Function.html. $\endgroup$– Jason RuteCommented Feb 20, 2023 at 18:31
-
$\begingroup$ @Jason Rute Of course it would help if I could include as tag words "analytic-number-theory" but the system does not allow it because I do not have 150 reputation points, which I think is totally silly ... as many things about the Stack platform are, but anyways, it is useful sometimes. $\endgroup$– EGMECommented Feb 20, 2023 at 20:54
-
$\begingroup$ @Jason Rute If you follow the links in the second link you provided, it seems a good chunk of Apostol's book is formalized in Isabelle. That is already a good starting point. Basically, it takes you halfway there to formalizing Ingham, which is the smaller of the two books I mention, and in a way, also the more useful and unrepetitively complete for lots of other stuff. I wonder if anything like this is done in LEAN $\endgroup$– EGMECommented Feb 20, 2023 at 20:59
-
$\begingroup$ I hesitate to give a formal answer since I don't know analytic number theory, but as for Lean, you can find out a lot on the Lean Zulip. First, just search for the topics you are interested, and second ask in Is there code for X? specifically about analytic number theory. (Or wait for someone more knowledgable than me to respond here.) The impression I get is that this isn't really in mathlib yet, but is being slowly worked on, and might depend on some prerequisites. You are likely welcome to pitch in. $\endgroup$– Jason RuteCommented Feb 20, 2023 at 23:58
|
Show 1 more comment