I'm surprised that nobody's mentioned Metamath, a proof language with a library of over ten thousand theorems and an open-source checker. Typically, the checker validates the entire library, but it doesn't take long. I would think it would be only a moderate project to get the Hex proof or the partitions proof in. Rodolfo Medina seems to be laying some of the groundwork for reasoning about partitions, though as far as I can tell he isn't counting them yet. On Mon, Mar 19, 2012 at 3:04 PM, Gareth McCaughan < gareth.mccaughan@pobox.com> wrote:
On Monday 19 March 2012 01:58:59 Henry Baker wrote:
Proof _checking_ is a purely mechanical, almost linear complexity (in the length of the proof) problem (depending upon the representation). _Finding_ a proof is the hard part, and can be multiply- (?) exponential in the length of the proof.
Clearly not multiply-exponential, given that proof checking is of approximately linear complexity. All you have to do is enumerate all possible proofs (there are singly-exponentially many) and check them one by one.
-- g _______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun