coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Number theoretic results

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Number theoretic results
Date: Fri, 4 Sep 2020 14:44:00 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wr1-f53.google.com
Ironport-phdr: 9a23:r08nqh2GkfNdGd68smDT+DRfVm0co7zxezQtwd8ZseIeKfad9pjvdHbS+e9qxAeQG9mCtbQd0bad4/mocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbalvIBmoogjducobjZZ/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6xbrxChqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TzuUEBrR+/BQa2Gejh1j5Ihnn53aIkyeQqDAbL3BA6H9IPtnTUo8v6NL0JXO+p16nE1zvCYOlN2Tf96YjIdB8hoe2LXbJ2a8be11QgFx7cg1iWtIfqMC+b2P4XvGiH8+pvS/ivi2g/pg1tvzSiyMghh4vGiI8Xyl7J9yZ0zYkoKdC6R0N2Yd2pHZVfuSybNIZ6X80vTW91tCs0xLMLupC2cDYExZk72xLSbeGMfYaP4hLmTumRIDF4iWp/d7K6nBa+60+gyvfzVsWs31ZKrzZFktnRtn8WzRDc9s+HSv5780y82jiPzxje5v9YLU0wj6bWKJ4szqQumpYNrEjPBC/7lUvwgaSLbEsr4PKo5P7iYrj+pp+TKYt0igbmP6QrgMO/AOA4PhEAXmiB5OiwzbPj8E33TblQgf02la7ZsJ/eJcsFvKK2HwhV0oM75xa+CTepzsgYkGEZIF5ZfB+LlYvkNlHULPzmE/uznk6gnTdlyvzeO73uGJTNLnzNkLf7erZ97lZRyBYpzdBe4ZJUBa8OIOjoV0Dtr9zUFBE4PBavw+bnCdV90IweWX6IAq+fKq/dr0KH5v83L+mWeIAVoCr9K+Qi5/P2kXA5nkYdcbC10psTdXC3Be9rI16ZYHrpmtcOC30Gvgs4TOzwiV2NSyRfZ3ioX/F02jZuI4W/SKzHW4rl1LeGxWKwGoBcTmFAEFGFV3nyIdaqQfAJPR6bJs5o2gYFU7esUcd1yQuvsgD30ZJsNazL8zYYtJTsyN9zoeDfiEdhpnRPE82B3jTVHClPlWQSSmpuhfEtkQlG0l6GlJNArbldHN1X6elOV15rZ5XHifNzENDzXA3dedHPRVq7EIz/XGMBC+kpytpLWH5TXtWviheZgnivCr4R0qORXdk6r/ma0H/2KMJwjX3B0ft51gV0co50LWSjw5VH2U3LHYeQwheSjOC1fL8c3SjC6GCFi2eCoRMAXQ==

You might have some luck looking through this for relevant theorems: http://www.ams.org/notices/200811/200811FullIssue.pdf

But less likely to be in Coq.

On Fri, Sep 4, 2020 at 12:30 PM Craig Fiedorek <rcraigfiedorek AT gmail.com> wrote:

There's a branch of math-comp that formalizes Cauchy-Schwarz:

https://github.com/math-comp/math-comp/blob/experiment/forms/mathcomp/algebra/forms.v

Best,
Craig

On Fri, Sep 4, 2020 at 3:04 PM Robert Rand <rnrand AT gmail.com> wrote:
Hi all,

Yuxiang (CC'd) and I were wondering if there are any formal proofs of the following theorems, ideally in Coq:

1) The Cauchy–Schwarz Inequality (over complex vectors)
2) Legendre's theorem
3) Bounds on Euler's totient function

Any pointers to closely related work would be a big help.

Thanks,
Robert

[Coq-Club] Number theoretic results, Robert Rand, 09/04/2020
- Re: [Coq-Club] Number theoretic results, Craig Fiedorek, 09/04/2020
  - Re: [Coq-Club] Number theoretic results, Talia Ringer, 09/04/2020