Classical error term in Isabelle!

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

The paper just came out today! https://www.isa-afp.org/browser_info/current/AFP/PNT_with_Remainder/outline.pdf So I'll read that over the next little while (I'm currently traveling...), and talk to Terry about what we'll want to do going forward. Perhaps we'll quickly finish Attack 2 (since we're really almost done), and resurrect Attack 3 to get the classical error, along the lines of the Isabelle formalization. Then on to Dirichlet, etc... More soon!...