coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Number theoretic results

From: Craig Fiedorek <rcraigfiedorek AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Number theoretic results
Date: Fri, 4 Sep 2020 15:30:21 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rcraigfiedorek AT gmail.com; spf=Pass smtp.mailfrom=rcraigfiedorek AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f41.google.com
Ironport-phdr: 9a23:uB3xcRYIkmWr+lOyjlFugpf/LSx+4OfEezUN459isYplN5qZr8m9bnLW6fgltlLVR4KTs6sC17OI9fm6BSdQuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLRi6txjdutcZjIdtKas91wbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrR2uqRxwwY7abo+WOvRjYK3SYcgXSnBdUstLTSFNHp+wYokJAuEcPehYtY79p14WoBagHwmjHuLvyjBVjXH23K01zfkuEQbc3AM+HNIFrXPZrM/pO6cIS++1zabIzTvCb/xIxDj975LIfQ4iofyXUrJwdNDeyUgrFw/fklqQronlMiqT2+8QvGeV8/BuWvizi247tQ5xuD6vy98ihITViIwZ1FDK+CV9zYs0JNC2R1J2bNG6HJZfqyyXOZZ7T8ciTmxpuys317kLtJy/cSUF1JkqxB7RZ+CHfoaG5B/oSeifITB9hH1/ebK/gQ6/8Uehyu3gVsm0zU1FojBZndnLs3AA0QHY5MufSvZl4EutxTKC2xrQ5+xEO0w4i7fXJpw7zrM/i5Yet1nIEDXsl0XslqCWc10p+ui25OTjZbXrvpqcOJV1igH6K6guhNe/DfkhPggAUGWX5P6w1LLk/U3+T7VKiuM5nrPFv5DdIMQXvq+5AwlL3YY/8xuzESuq3dACkXQELF9JYgyLg5XrNl3UL/30EO+zg1G2nzdqw/DGMKfhApLILnXbirfuYax95FRdyAo8w9Bf5oxbBawGIPLpREDxt8fVDhA8MwOuwubnDM9x2Z8ZWWKKGqOZKr/dsUeU5uIzJOmBfJMauDHkK/Q8+/HuiWI5lkQGcKmy3ZoXbWi4Ee58L0WYZ3rsmNYBHn0QsgowVuy5wGGFBDVUfjO5W782zjA9EoOvS4nZFa63h7nU9z2yH5IeSGFLBleWHHSgI5+PQf4NZyyTL8NmiDEHfbekQo4lkxqpsVmpmPJcMuPI93hA5trY399v6riLzE1gxXlPF82Yllq1YSRshGpRHm052al+pQp2zVLRifEp0cwdLsRa4rZyail/MJfdy+JgDNWrA1DOe96ITBCtRdD0WGhsHOJ0+McHZgNGI/vnjh3H2HD3UboclrjOGodtt6yAhj7+IMFyz3uA364k3QEr

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