coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alex Shkotin <alex.shkotin AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] π>e
- Date: Sun, 24 Oct 2021 10:48:52 +0300
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex.shkotin AT gmail.com; spf=Pass smtp.mailfrom=alex.shkotin AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f44.google.com
- Ironport-data: A9a23:4Q3ycKPFTCYoQCjvrR3GlsFynXyQoLVcMsFnjC/WdQnr1jh302NUmDQXWWuFOqnfazT8KYp2aYnip0sBsJTVv4NqS1BcGVNFHysb85KdbTi6Bh6tZH3KdpWroHqKXqzyU/GYRCwPZiKa9kjF3oTJ9yEmjPjQHOGkVIYoBwgoLeNaYHd54f5cs7Vh6mJYqYDR7zKl4bsekeWHULOW82Ic3lYv1k62gEgHUMIeF98vlgdWifhj5DcynpSOZX4VDfnZw3DQGuG4EgMmLtsvwo1V/kuBl/ssItask7K+c0pTB7COYU6BjX1ZX6XkiR9HzsAw+vxjZbxMNAEO1WvPw4wZJNZl7fRcTS8gOqDc3v8dUB5EEidWMqhP+buBKn+62SCW5xSYKCO9nZ2CC2lvZdFCkgptOklF8uVdIzQQZDiYlueuyfS6TPNtj4ItNqHW0Ck3rik1l3eGGa9zGdabV/+fvZkCjWZpkpsbRbCDc5VMQCRLRxHkTx1rG14xNIgaouaNkiCnJmYc8QqBzUYsy23azQg00b+0ddSJJpqFQsJamkverWXDl1kVyyoybLS3oQdpOFr17gMOoc/6ZG7WPLix9/ovgVrKg2JPVFsZUly0pfT/gUm7Mz6aAyT45QJ2xZXeNmTyJjU+Y/F8iHGBtx8YHdFXFoXWLSmTn7HM7V/x6ncsF1Z8hR9PiCPybTMv316N2djuAFSDdZX9pW21rt+pkN95BcTZwaLuq8PJocvpLuQPeL0Osy8=
- Ironport-hdrordr: A9a23:Hvp7VKi+jPch8gZ1vGNpC5ZNuXBQXscji2hC6mlwRA09TyX4rbHMoB11726QtN98Yh8dcLO7WJVoP0msl6KdiLN5VdzJYOCBggqVxepZgbcKrQeMJ8SHzIFg6Zs=
- Ironport-phdr: A9a23:4AWvOxJooxO2jwbRcNmcuORmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvbM31wWCBdSTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fNbwhGmjaxbq9+IRGrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs7Xims77pwSB/wligIKyI5/m/Qisx1lq1boRShrAF7z4PbZIyZMfxzdb7fc9wHX2pMRsleVyJDDY28YYUBDPcPM/hEoITmvVQCsQGzCBOwCO/zyDJFgGL9060g0+QmFAHLxBAtH9YQv3Xbsd77KacSUeOyzKnUzDXDae5d1DDn54jMbB8gruuAXalwccrSzkkvCwLFjlOLpIzqOjOazOUNs2yB4+V8UuKvjncqpgdsqTeg2skikJPGhp4Jyl/a7yV5xp44KcC6RUN7ZdOoDptduiOaOYZ3Qs4vQH1ktik6x7ACpZK2fzUHxYkmyhLDb/GJfIeG7xP9WOuePzt2i3Boda+xiRu07EOuxOr8Vsyu31ZLqCpIitbMtncK1xzc7siIVOFx8Vum2TaKzwzT5eBEIVw0larGMJEt2KI/lp0WsUjbAiD2n1/2jKmIeUUg/uik8frobaj7ppKaKoR6iRn+P7wwlsCjBek0KAsDUmiB9eih1bDu/Ff1TbpFg/Awj6LXqorVJd4Bqa68GwJV0pgs6xK4Dzq+1dQXh3gHLFZcdBKGiIjlJkjCIP73APqwmVisnzBrx/fJPr3lHJrBNGTMkLDkfbpl6k5czhQ8zcxH6p5KFr0MJOj/V0zxudDCExM0Mg25z/zoBdhyzo8eXHiAAq6dMKPcq1+I4ecvLvGWa48Rpjn8JOIp5+XujX86nl8dYaip3Z0MZXC3G/RpOUSZYX72jtgdFmcKuxIyTPb2h12aTT5Te3GyUrog6TE8EYKqFJvMRoSwgLOaxyq7BZ1XZmVeCl+WC3vodoOEW+0NaC2IOMNhnCYEBvCdTNoq0gjrvwvnwZJmKPDV82sWr8HNzt9wssTXmAF6zjx3CNic1SnZRmV5jiUTRzwxwKF5iUN4w1aHl6N/hqoLRpRo+/pVX1JiZtbnxOtgBoWuC2opm/+GTV+nRpOtBjRjFrrZLPcBZk98H5OpiRWRhkJC4pcQnr2PQZ0zq+fSgyS3KMF6xHLLkqImigt+KvY=
Thanks, Abhishek and All!
The origin of my question is here https://groups.google.com/g/ontolog-forum/c/q9XT9WCxM_c
Alex
вс, 24 окт. 2021 г. в 08:02, Abhishek Anand <abhishek.anand.iitg AT gmail.com>:
for any 2 closed, computable real numbers r1 r2, r1>r2 can be proved automatically if it is true: just compute enough "digits" of r1 and r2, as Agnishom suggests. \pi and e are computable and are already defined in the CORN library in a computable ("constructive") way that lets you COMPUTE arbitrarily tight Q approximations to them.-- Abhishekhttp://www.cs.cornell.edu/~aa755/On Fri, Oct 22, 2021 at 11:44 AM Alex Shkotin <alex.shkotin AT gmail.com> wrote:Hi All!How in Coq define π and e and prove that π>e?Alex
- [Coq-Club] π>e, Alex Shkotin, 10/22/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/22/2021
- Re: [Coq-Club] π>e, TJ Machado, 10/22/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/24/2021
- Re: [Coq-Club] π>e, Abhishek Anand, 10/24/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/24/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/25/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/25/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/25/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/25/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/25/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/25/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/25/2021
- Re: [Coq-Club] π>e, Alex Shkotin, 10/24/2021
- Re: [Coq-Club] π>e, Agnishom Chattopadhyay, 10/22/2021
Archive powered by MHonArc 2.6.19+.