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 :-)
>> 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.
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev