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
