coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can you name the biggest number?

From: roux cody <cody.roux AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Can you name the biggest number?
Date: Sat, 30 Nov 2019 19:06:14 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cody.roux AT gmail.com; spf=Pass smtp.mailfrom=cody.roux AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f51.google.com
Ironport-phdr: 9a23:w6UcixVK+aCyYatv9OXVUdQ6uxjV8LGtZVwlr6E/grcLSJyIuqrYYxaCt8tkgFKBZ4jH8fUM07OQ7/m7HzVfu93Y7DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrowjdrNQajIl8Jqo+1xfErWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNww4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDrQG5BQmxC+Lk1yNHhnjr0qw6zu8sFh3J3As9ENMOqnjUttL1NLodUO2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltf8TRzkwvGBnEjlWWsYHlMDKV1vgNs2iG9OVsT/6gi2kiqwx3vzOhxd8sh5HXio4Jzl3I7yZ0zYYvKdGmVUJ2Y8SoHZtNuyycKoB4WNktQ3tytyY/0rAGuYC0fCwNyJk/wh7Qcf2Hc4yR7hL9T+adPC50hHxldb6inRqy/k+gyurzVsmwzllGtDZKkt7JtnwV1hzT7NaISudl80u/xTqC0xrf5+JELEwui6bXNpwszqQwm5YOqUjDGzX5mETyjK+YbEUk/e2o5vz7bbXhu5CdN5V4ihv5MqQzlc2yGus4Mg0UUGia/eSwzqHs/Ur8QLlSlP05jrHZsIzGJcQcvqO2HwhV0p865xmjCzemzc8XkGIcLFNFfRKHl5LmN0vPIPD+F/e/gk6jnC1lx/DcbfXdBcDGKWGGm7P8d5587VRdwUw914Nx/ZVRX6sGPeK7UUj9pZSMBRg1IkquxPv3INp434IaH2mIB/nKY+vprVaU67d3cKG3b4gPtWOlcql317vVlXY83GQlU+ys1JoTZmq/G60/cUqcaHvoxNwGFDVT51dsfKnRkFSHFAVrSTOyUqY7vGxpDYunCcLdXdnojuHYmii8GZJSayZNDVXeSS60JbXBYO8FbWepGuEkiiYNDOHzRIoo1BXovwj/meJq

Hi all,

I'd like you invite the enthusiasts of Coq and proof theory in general to participate in a small and fun ongoing challenge, which I have hosted on Github for lack of better ideas (but I'm open to suggestions):

https://github.com/codyroux/name-the-biggest-number

The rules are relatively simple: name the biggest number, and prove it! More specifically, the objective is to take the current "contender", which is a coq definition of type nat and provide a definition of some different number and a proof that it is larger. Past contenders are kept in the "graveyard". The actual rules can be found in the README.

Things are still quite small at the moment (ackermann-ish), so a lot is up for grabs! Termination analysis techniques should help, but I suspect proof theory will pull ahead in the end.

Happy hunting!

Cody

[Coq-Club] Can you name the biggest number?, roux cody, 12/01/2019
- Re: [Coq-Club] Can you name the biggest number?, Emilio Jesús Gallego Arias, 12/02/2019
  - Re: [Coq-Club] Can you name the biggest number?, roux cody, 12/02/2019
    - Re: [Coq-Club] Can you name the biggest number?, Emilio Jesús Gallego Arias, 12/02/2019
    - Re: [Coq-Club] Can you name the biggest number?, Thorsten Altenkirch, 12/02/2019