Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On the other side, proof automation and formalization has gained more and more steam, culminating at, for example, recent efforts by Gonthier et al. to encode the Feit-Thompson theorem, and this trend will not stop as homotopy type theory has become a hot research topic. It then only seems natural to ask what open problems or technical challenges still lie ahead before we arrive at a Google Books style of automatically extracting human proofs written on paper (or just in latex) to formalized and checked proofs in something like Coq?

Ideally, answers regarding both the mathematical side and the more empirical machine learning side (or perhaps other viewpoints I've not considered here) are welcome, but I'm not quite sure if the latter is on topic on mathoverflow. And ideally, I should think we want to avoid babbling philosophy here, e.g. what's the point of mathematics, etc.