Scripting math proofs with RHilbert

Formal math projects like wikiproofs prove mathematical theorems in a way that a computer can verify. There could be several motivations for this, including finding/preventing errors in proofs, helping learners to understand a proof, or exploring the consequences of assuming a different set of axioms.

Wikiproofs and related projects like metamath require that the person writing the proof spell it out pretty explicitly. For example, if you have 1 + 2 = 3 and you need 2 + 1 = 3, you'll need to explicitly transform one into the other. Other proof systems, like coq and isabelle, have a fairly powerful prover which can notice that you have 1 + 2 = 3 and a + b = b + a and combine those to prove 2 + 1 = 3.

Enough background. What I've been playing with lately is a project I just started and which I am calling Hilbert. This is a marriage of a metamath-like proof engine (in this case hilbert-kernel) and a generic scripting language (in this case Ruby). Writing a full prover in Ruby is of course one direction this could eventually head, but I was thinking more in terms of simpler kinds of automation (perhaps there could be a routine called "commute as needed" which would be able to turn "1 + 4 = 3 + 2" into "4 + 1 = 3 + 2" by noticing the left hand side needs to be flipped and the right hand side doesn't). I'm hoping this system will be easy for people who find Ruby more comfortable than coq or isabelle (I might count myself among them, although of course I reserve the right to learn coq or isabelle some day). It also may have other benefits, like making it easier to develop hilbert-kernel itself (for example by running hilbert-kernel tests).

Update 20 May 2011: this is under active development, but the change which needed an update above is that I renamed the project from RHilbert to hilbert.