> ... an open source "math compiler" ... Automated theorem provers behave much like this. As you lay out the steps of a proof they will check that each step is

> ... an open source "math compiler" ... Automated theorem provers behave much like this. As you lay out the steps of a proof they will check that each step is correct and show you what you have remaining to prove. You can start with a vague proof outline and refine each step until there is enough detail for the compiler to infer a full formal proof. Check out the Isabelle/HOL tutorial for a good example: http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.... These tools are still very young but they have already proved useful in cutting edge research eg http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf http://research.microsoft.com/en-us/um/people/gonthier/4colp...