I saw the following (redacted, numbers modified) section in a recent paper doing a long proof in an interactive theorem prover:

Statistics

My proof, excluding standard libraries and the library for foobaring bazes, consists of 33 source files, 9 136 lines of specifications, 37 101 lines of proof, and 1 255 709 total characters. The size of the gzipped tarball (`gzip -9`) of all the source files is 135 009 bytes, which is an estimate of the information content of my proof.

Call me a stat-hater, but I found the last line somewhat ridiculous. What next? Every paper must have a section

The size of the gzipped (gzip -9) pdf file for this paper is XXX bytes, which is an estimate of the information content of this paper.

A nice fixpoint problem to find XXX, though!

### Like this:

Like Loading...

*Related*

This entry was posted on April 18, 2012 at 7:45 am and is filed under Uncategorized. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

July 9, 2012 at 4:16 pm |

Á propos, http://xkcd.com/688/