Artificial Mathematical Intelligence in 2025
Artificial Intelligence can be applied to many math-related tasks, including formal and informal theorem proving, formalization and informalization, and math discovery. In order to make long term progress, it is necessary to have a good understanding of each task, of their relationships, and of what is currently within reach.
Why math should be formalized - and resources to get started
Proof assistants enable us to formalize mathematics: to express arbitrary mathematical statements and proofs without ambiguity, and to automatically verify their correctness. Here I give some arguments for why math formalization might soon become inevitable. I also include some resources on formalization for the interested reader.
Cover Learning for Topological Inference
The standard approach to Topological Inference is based on geometric complexes. Most commonly, geometric complexes scale cubically (and often worse) in the number of data points, which poses a big problem. Here I describe an alternative approach to Topological Inference.
Topological Inference and Unsupervised Learning
Fundamental problems in Unsupervised Learning, such as Clustering and Dimensionality Reduction, can be fruitfully interpreted from the point of view of Topological Inference. This is an introduction to this point of view.