coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Number theoretic results

From: Robert Rand <rnrand AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Cc: Yuxiang Peng <pickspeng AT gmail.com>
Subject: [Coq-Club] Number theoretic results
Date: Fri, 4 Sep 2020 14:03:45 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rnrand AT gmail.com; spf=Pass smtp.mailfrom=rxtreme AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f172.google.com
Ironport-phdr: 9a23:PwtAGhKTIFUxMcvXR9mcpTZWNBhigK39O0sv0rFitYgeKPrxwZ3uMQTl6Ol3ixeRBMOHsqwC0rCK+PC5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe8bL9oMRm6swrcusYVjId/N6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhTwZPDAl7m7Yls1wjLpaoB2/oRx/35XUa5yROPZnY6/RYc8WSW9HU81MVSJOH5m8YpMAAOQBM+hWrJTzqUUSohalHwagGPnixyVUinPq36A31fkqHwHc3AwnGtIDqGjarNLuO6gMS+C10LTDwynZYPNQxDj29Y/FcgonofGWR71wd9fexFIgFwPAlFqQqIjlMymJ2eQKtmiW9uxtXv+ghGA7sQ9+uCSvxtsyhYnTgIIY0l7K+DlnzYopOdC1R1N3bcK4HJVQqS2UOY97Tt0jTmxpuys21rMLtIC7cSYKyZkr2wPTZfyFfoaG4B/uSOifLCp+iXl4e7y/nw6//Va8xuD4TMW501ZHojBbntXRsn0BzQHf58qZRvZ740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5ocq0XDHivvlET2l6Caa1wo+ua15+nlfLnqvJCcN4hzigHxNqQhhNazDvg/MggLR2Sb+OK826P//UDhXrlGkvk7nrPavZ3aP8gXuLO1DgtP3oo+6RuzES+q0NECknkGKFJFdgiHj4/sO1zWOvD5Auu/g06ynzdu2f/LJbLhApDXIXjClLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioSnkZVVq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/slqIXCRPL0y7Wa50sis9EougAa/MQ4mshPqK2yLtTc4eXXxPFl3ZSSSgTI6DQfpZLXvKepY8wAxBbqCoTsoa7T/rtAL+zOA5fO/d+yldpJi6kdYsuLeVmhY1+jh5Sc+a1jPVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUBR9NW7vJNFAw9MMyFlrAoO5XJQgvEO+yxZhO+WNz/WGM+S9swx5kFZEMvQ9g=

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