I think it supports strangestchild's thesis that all five proofs from this page[1] would fit on a page and a half printed but the Coq proof (the only one I could find a download for from your list) is 825 lines of code.
Yes, well, I suppose I could fit all of Firefox on one page as long as you only look at the main() function and not any of the functions that lead up to it. But that doesn't really tell you much about Firefox, does it? And the fact that there are primitives like pthread_create() and pow() underneath at sufficiently low level doesn't really say much either.
I think it supports strangestchild's thesis that all five proofs from this page[1] would fit on a page and a half printed but the Coq proof (the only one I could find a download for from your list) is 825 lines of code.
[1]: http://primes.utm.edu/notes/proofs/infinite/
You can easily fit all of them on one page, as long as you build enough scaffolding theorems to get there.
I am not that familiar with the field, but http://us.metamath.org/mpegif/infpnlem2.html fits on one page. If you fully expand the proofs of each subclause, I don't know how long it is, but it won't fit on a page. You will get through to the 'bloody obvious', though, with such things as http://us.metamath.org/mpegif/syl.html "if A implies B and B implies C, then A implies C", which this system proofs from http://us.metamath.org/mpegif/a1i.html "if A is true, then anything implies it" and http://us.metamath.org/mpegif/ax-mp.html "if A is true and A implies B, then B is true"
Yes, well, I suppose I could fit all of Firefox on one page as long as you only look at the main() function and not any of the functions that lead up to it. But that doesn't really tell you much about Firefox, does it? And the fact that there are primitives like pthread_create() and pow() underneath at sufficiently low level doesn't really say much either.
1 reply →