"in practice automated theorem proving is almost useless - just mindless search - computers only beat humans at ‘puzzles’ - don’t expect computers to produce interesting proofs on their own"

Bij wiskundigen die met automatische bewijsprogramma's werken zie ik vaak dezelfde afwijzende houding tegenover het volledig formaliseren van wiskunde. Zo schrijft Ursula Martin in "Computers, reasoning and mathematical practice", Computational Logic, Vol. 165 (1999), pp. 301-346 het volgende:

"The latter [full formal development of large bodies of mathematics] is at odds with mathematical practice: many mathematicians view formal proof development unsympathetically and it is hard to see it being incorporated except in expensive reworkings of well-understood material."

Ik vraag me af waaruit deze wederzijdse afwijzing voorkomt. Hebben we hier met twee verschillende 'culturen' in de wiskunde te maken? De 'formele' versus de 'pragmatische' wiskundigen?