Even if you didn’t do Timothy Gowers’s questionnaire the first time around, you will be fascinated by his explanation of its hidden purpose and will want to do his follow-up poll.
Update: And you will now be fascinated by Gowers’s report on the experiment.
Is there some further trick to it? It’s been a while since I knew what was the state of the art in automatic theorem-proving, but I’d be surprised (and certainly interested) if it had got as far as those posts makes it seem, and a new theorem prover is not something that can be dashed off casually. I had to check the date of the second post to make sure it wasn’t April 1st.
Gowers’s collaborator recently did a thesis on the language of mathematics which I see is available as an interesting-looking book, but while that might help with the language aspect, I don’t think it would give them a theorem-prover.
Well, Mohan Ganesalingam is seriously good (Senior Wrangler for a start, I believe): and I suppose there are existing theorem provers on the top of which you can sit a “natural language for mathematicians” module of the kind he has been working on for years. But we’ll await more details. In the meantime, thanks for the info that Mohan’s book is out.