Note that there are formal, machine-checkable languages to describe geometric proofs: http://lambda-the-ultimate.org/node/3899 http://lambda-the-ultimate.org/no

Note that there are formal, machine-checkable languages to describe geometric proofs: http://lambda-the-ultimate.org/node/3899 http://lambda-the-ultimate.org/node/3899 Of course, that still leaves the same problem of explicit proofs being tedious, i.e. being able to prove pythagoras's theorem "with a diagram" does not mean being able to prove it "within an explicit, formalised diagram language".