The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Someone else just pointed this out to me! As I was saying, I'd be happy to declare this the winning entry, as long as it was formalized in Coq and proven to be larger than current contender :).

Cody

On Mon, Dec 2, 2019, 8:18 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

roux cody <cody.roux AT gmail.com> writes:

>     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

It is worth recalling the winner of the BIGNUM BAKEOFF contest by Ralph
Loader: http://djm.cc/bignum-results.txt

,----
| The final and winning entry, {loader.c}, diagonalizes over the
| Huet-Coquand `calculus of constructions'.  This is a highly polymorphic
| lambda calculus such that every well-formed term in the calculus is
| strongly normalizing; or, to put it another way, a relatively powerful
| programming language which has the property that every well-formed
| program in the language terminates.  The program's main function is
| called D.  (D's return value depends on a global variable, so it is in
| fact not a pure function, but this will not be important.) D works
| approximately as follows: given an argument x, it iterates over all bit
| strings with binary value less than or equal to x, and, if such a bit
| string codes for a well-formed program (`term' in lambda-calculus
| language), it runs the program (`strongly normalizes the term' in
| lambda-calculus language.)  The return value of D is then obtained by
| packaging together the return values of all these programs.  The
| program's return value is D@@5(99).  It is possible to simulate the
| computation of D(99) and prove that D(99) >= E(30419).  Also, it is easy
| to prove that D(z) >= z and that D(z) is increasing with z.  Therefore,
| the value output by the program is at least D(E(30419)).  However, in
| {FLO}, Fortune et al.  explain how to code F[omega**k] and F[epsilon_0]
| in the second-order typed lambda calculus.  The second-order typed
| lambda calculus is a subset of the calculus of constructions, and the
| methods in {FLO} can easily be used to code, say, F[epsilon_0 +
| omega**3](1000000) in a relatively short program, which can be expressed
| by a bit string of length well under E(30419).  {loader.c} is therefore
| the winner.
`----

E.