Towards Artificial Mathematical Intelligence (AMI)

What are the formal (meta-mathematical) bounds for developing a software being able to find human-style solutions for general (solvable) mathematical conjectures?

There is a quite natural and practical question within the foundations and origins of computer science (and mathematics) that needs a deeper answer: how much of current mathematics (i.e. mathematics described in contemporary mathematical journals) can be completely generated by a computer program? In other words, how near are we for constructing (programming) a machine which can simulate the way a modern working mathematician usually faces a solvable mathematical conjecture, works some time on it, and finally finds a formal solution for it?

Here it is important to clarify that the main purpose of the former question is to ‘meta-model’ and ‘meta-simulate’ the general modern mathematician in the specific intellectual activity of receiving a con- crete conjecture (which can be solved within the mathematical framework), working on it and finally giving a clear answer, i.e., writing a (formalizable) solution to the conjecture in the form of either a proof or a counterexample (or sometimes a proof of its ‘independence’ from the corresponding axiomatic system).

Besides, because the former questions involve implicitly the mathematician’s mind, we should take inspiration from the current most relevant cognitive theories concerning mathematical reasoning and closely related matters. The most successful theories that we currently have for understanding how our mind works are theories with a formal computational conceptual basis like the computational theory of mind. This fact can be seen as a form of ‘heuristic’ support for the thesis that it is possible to meta- model, (formally and computationally) the intellectual job of a working mathematician. A second theoretical support is the fact that modern mathematics are essentially founded and (at some level)

'conceptually delimited' on Zermelo-Fraenkel Set Theory with Choice (ZFC), proof, recursion, and model theory.

That means that the solution of a solvable conjecture should be precisely described as a formal (logi- cal) consequence of the axioms of ZFC, using a finite (or recursively generated) number of inference rules and initial premises. In other words, when a mathematician finally finds a correct solution of a conjecture, then the result of his/her research is simply a kind of computation of a theoretically-feasible computer program, which starts to run all the possible proofs of provable theorems of ZFC, starting from a finite sub-collection of axioms and following precise (logical) mechanical deduction rules. Here it is important to mention that we are focusing on solvable conjectures, i.e., on problems having an explicit formal proof or counterex- ample within the ZFC framework. These problems constitute mathematics being studied by at most of the mathematicians today, and these are the ones producing most of the concrete applications. So, we will call this problem Artificial Mathematical Intelligence (AMI), i.e., the construction (implementa- tion) of a computer program being able to solve essentially every human solvable mathematical conjecture in less time than an average professional mathematician; and subsequently to generate also human-style

independence proofs for undecidable conjectures. Now, although concerns about undecidable

issues are clearly important from a purely theoretical perspective, within our AMI meta-project

the decidable sentences are the central focus of attention.

For more information see the official website https://dagomez1982.wixsite.com/artmathintelligence