When David Hilbert started so called "Hilbert's program" (formalization of mathematics) in the early 20th century to give a solid foundation to mathematics, he unintentionally introduced the possibility of automatization of mathematics. Theoretically, the possibility was denied by Gödel's incompleteness theorem. However, an interesting issue remains: is "mundane mathematics" automatizable? We are developing a system that solves a wide range of math problems written in natural language, as a part of the Todai Robot Project, an AI challenge to pass the university entrance examination. We give an overview and report on the progress of our project, and the theoretical and methodological difficulties to be overcome. Copyright is held by the owner/author(s). Publication rights licensed to ACM.