AI/TP Methods for maximizing generality and tractability of algebras

Gonçalo Gomes Araújo

PhD at Nova FCT

We value a mathematical theory for its generality and its tractability. For example, a magma (that is, a set with a binary operation) is very general because any theorem on it will have an impact on almost all algebras and possibly beyond, but the structure is so weak that deep theorems are very difficult to prove. The goal of this project is to use Artificial Intelligence Theorem Proving (AITP) tools and AI techniques to devise new mathematical theories, maximizing generality and tractability. We expect to find several theories that will have a good ratio of generality/tractability that might be explored in the future. In addition, we will have many theories with a high level of generality where tractability might be proved once sufficiently strong AITP tools are available.

Keywords: Mathematics, AI, Class of Algebras, Prover9, AITP, Partial Ordered Set

Scientific area: Mathematics and Artificial Intelligence

Bio: I am a PhD student at the Department of Mathematics of the NOVA School of Science and Technology, and currently I am working in Computational Algebra with Professor João Araújo and Professor Josef Urban, generalizing well known mathematical sets, such as groups, quasigroups and inverse semigroups. My main research interest is applying Artificial Intelligence Theorem Provers to prove important properties and theorems regarding those classes of algebras. In 2020, I finished my Bachelor’s Degree in Mathematics, being awarded in 2018 for being the best student in the first year of my Bachelor’s Degree. After that, I obtained my Master’s Degree in Pure Mathematics in 2022, and in my Master’s Thesis I worked with important equivalences between Uniformly Almost Periodic Functions.

Visiting period: May – August 2024 at Department of Automated Reasoning at CIIRC