Name: Anonymous 2014-06-01 20:28
Gödel didn't need a proof assistant, why do you? You'll never succeed in making maths entirely computable, automatable, never.
implying there's no such thing as data mining.things computers notoriously bad at.implying patterns can't be extrapolated from data