I am wondering if there are any plans to create an importer for the problems from TGTP http://hilbert.mat.uc.pt/TGTP/index.php in Mathematica? A similar site for the theorem provers is TPTP: http://www.tptp.org/ - it would also be cool to have an interface to that too...
