Note: [1] This is an extended and updated version of a talk at the 1st Conference on Artificial Intelligence and Theorem Proving and a paper entitled “Race against the Teens – Benchmarking Mechanized Math on Pre-university Problems” published in the proceedings of the International Joint Conference on Automated Reasoning 2016 (IJCAR 2016) [33]. All the statistics and the experimental results are updated using the latest public version of the benchmark data and the current version of the prototype solver.
Abstract: This paper introduces a benchmark problem library for mechanized mathematics including computer algebra and automated theorem proving. The library consists of pre-university mathematical problems taken from exercise problem books, university entrance examinations, and the International Mathematical Olympiads. The subject areas include real algebra, geometry, number theory, pre-calculus, calculus, and combinatorics. It thus includes problems in various areas of pre-university mathematics and with a variety of difficulty. Unlike other existing benchmark libraries, this one contains problems that are formalized so that they are obtainable as the result of mechanical translation of the original problems expressed in natural language. In other words, the library is designed to support the integration of the technologies of mechanized mathematics and natural language processing towards the goal of end-to-end automatic mathematical problem solving. The paper also presents preliminary experimental results of our prototype reasoning component of an end-to-end system on the library. The library is publicly available through the Internet.
