The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

Dear Coq clubbers,

In this programming competition

https://codingcompetitions.withgoogle.com/codejam

Google challenges the participants to solve computing problems as fast as possible, in any programming language. Both the time to program the solutions and their execution time count in the competition's ranking.

Usually the problems are stated in terms of natural numbers and the execution time limits prevent brute force algorithms. So you often have to come up with twisted formulas with many edge cases, and hope that your results will match those of Google.

I have seen many videos on the web and posts on Stack Overflow giving usual pen-and-paper mathematical proofs of the algorithms, but so far I haven't found a Coq database with the corresponding formal proofs. Does it exist somewhere, maybe for another programming competition ?

If not, I think it would be nice to do it. First it's fun : it fully explains why the black magic formulas do solve the problems. Second, it would give some visibility to Coq among the competitors of the code jams, who are good developers. A collaborative database would be best, where anyone can push a proof when they finish it. Do you know a natural place to put this database ?

Regards,

Vincent