[isabelle-dev] Old_Number_Theory

Manuel Eberl eberlm at in.tum.de
Tue Oct 18 13:33:38 CEST 2016

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.



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 <eberlm at in.tum.de 
>> <mailto:eberlm at 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-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161018/26eda18a/attachment-0002.html>

More information about the isabelle-dev mailing list