Resources

While numeric and symbolic computation have long been mechanized, the Institute for Computer-Aided Reasoning in Mathematics focuses on computational technologies that can assist mathematical reasoning and discovery more broadly, specifically, formalization and interactive theorem proving, automated reasoning and symbolic AI, and machine learning and neural AI.

Formalization and interactive theorem proving involve the use of computational proof assistants to represent mathematical definitions, theorems, and proofs in precise, digital formats that can be checked and processed by a computer. This makes it possible to verify the correctness of mathematical proofs, down to axiomatic primitives. Like the digitization of language, however, the digitization of mathematics is more generally useful. Proof assistants are being used to build communal mathematical libraries that can be searched, updated, and maintained electronically. They open up new ways to share and communicate mathematical knowledge, as well as new forms of collaboration. They also offer ways to use symbolic and neural AI.

Automated reasoning and symbolic AI provide logic-based methods for mathematical reasoning, verification, and discovery. These include search procedures, which carry out open-ended searches for mathematical objects and/or proofs, and decision procedures, which are deterministic algorithms for deciding the truth of mathematical claims in various domains. Automated reasoning tools can be used without formalization, but they can also support formalization, and conversely, formal methods can be used to verify the correctness of such algorithms.

Machine learning and neural AI provide systems that learn a model from either static data or interactive exploration, and use that model to carry out inferences. The models can be simple, for example, a linear model or a decision tree, or they can involve billions of parameters in a complex neural network. Such systems can contribute to mathematics in many different ways, some involving formal methods and symbolic AI, and some entirely independent.

All three areas come together in neural theorem proving, i.e., the use of neural networks to prove mathematical theorems automatically. Some contemporary systems make central use of formal mathematics, formal libraries, and symbolic tools, and yield formally checked proofs as output. Others operate primarily, or even solely, in natural language.

ICARM aims to help mathematical researchers leverage these technologies. Our resource pages currently provide survey overviews, notable examples, and links to online resources, tutorials, and communities. Over time, we will provide additional computational resources, tutorials, evaluations, and training and technical support.