<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font size="+1">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)</font></p>
<p><font size="+1">So I think if anyone wants to work on this in the
future, I think we have a lot of nice building blocks available.</font></p>
<p><font size="+1">Cheers,</font></p>
<p><font size="+1">Manuel</font><br>
</p>
<br>
<div class="moz-cite-prefix">On 18/10/16 13:27, Lawrence Paulson
wrote:<br>
</div>
<blockquote
cite="mid:C62C7E8A-934B-4634-8EE2-2D14D4B4D32A@cam.ac.uk"
type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
That is great news!
<div class=""><br class="">
</div>
<div class="">It’s a pity that our coverage of number theory is
minuscule compared with what we have for analysis. I blame John
Harrison :-)</div>
<div class=""><br class="">
<div class="">
<span class="Apple-style-span" style="border-collapse:
separate; color: rgb(0, 0, 0); font-family: Helvetica;
font-size: 11px; font-style: normal; font-variant: normal;
font-weight: normal; letter-spacing: normal; line-height:
normal; orphans: 2; text-align: auto; text-indent: 0px;
text-transform: none; white-space: normal; widows: 2;
word-spacing: 0px; -webkit-border-horizontal-spacing: 0px;
-webkit-border-vertical-spacing: 0px;
-webkit-text-decorations-in-effect: none;
-webkit-text-size-adjust: auto; -webkit-text-stroke-width:
0; ">
<div class="">Larry</div>
</span>
</div>
<br class="">
<div>
<blockquote type="cite" class="">
<div class="">On 18 Oct 2016, at 12:11, Manuel Eberl <<a
moz-do-not-send="true" href="mailto:eberlm@in.tum.de"
class="">eberlm@in.tum.de</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<meta http-equiv="content-type" content="text/html;
charset=utf-8" class="">
<div bgcolor="#FFFFFF" text="#000000" class="">
<p class=""><font class="" size="+1">I am glad to
announce that as of</font><font class="" size="+1">
<meta http-equiv="content-type" content="text/html;
charset=utf-8" class="">
261d42f0bfac, Old_Number_Theory is finally history.</font></p>
<p class=""><font class="" size="+1">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.</font></p>
<p class=""><font class="" size="+1">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.<br class="">
</font></p>
<p class=""><font class="" size="+1"><br class="">
Cheers,</font></p>
<p class=""><font class="" size="+1">Manuel<br class="">
</font></p>
</div>
_______________________________________________<br
class="">
isabelle-dev mailing list<br class="">
<a moz-do-not-send="true"
href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br
class="">
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br
class="">
</div>
</blockquote>
</div>
<br class="">
</div>
</blockquote>
<br>
</body>
</html>