True, but even though I am hardly an expert in number theory, I would imagine that a solid foundation in analysis (especially complex analysis) is very helpful, if not indispensable, in the development of advanced number theory. (the most obvious example is the complex-analytic proof of PNT and the Riemann ζ function)

So I think if anyone wants to work on this in the future, I think we have a lot of nice building blocks available.


Cheers,

Manuel


On 18/10/16 13:27, Lawrence Paulson wrote:
That is great news!

It’s a pity that our coverage of number theory is minuscule compared with what we have for analysis. I blame John Harrison :-)

Larry

On 18 Oct 2016, at 12:11, Manuel Eberl <ebe...@in.tum.de <mailto:ebe...@in.tum.de>> wrote:

I am glad to announce that as of261d42f0bfac, Old_Number_Theory is finally history.

A lot of the proofs are still quite messy and don't take advantage of the new features we now have in Number_Theory (such as a uniform concept of ‘primes’ and ‘prime factorisations’ for both nat and int), but I do not think the work necessary to achieve that is worth it.

The vast majority of the porting work was done by a student of ours, Jaime Mendizabal Roche, so big thanks to him. He even extended the ‘two squares’ AFP entry a bit, showing the converse direction as well.


Cheers,

Manuel

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to