There is a quite natural and practical question within the foundations and origins of mathematics that needs a deeper answer: how much of current mathematics (i.e. mathematics described in contemporary (mathematical and closely related) 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 researcher 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 to ‘meta-simulate’ how a human being (abstractly) ‘handles’ regarding the specific intellectual activity of receiving a concrete conjecture (which typically can be solved within a standard 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 human’s mind, one 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. So, 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 (mathematical) job of a human being.

A second theoretical support is the fact that modern mathematics is essentially founded and (at some level) 'conceptually delimited' on (Zermelo-Fraenkel) Set Theory with Choice (ZFC), proof, recursion, and model theory.

This means that the solution of a solvable conjecture should be precisely described as a formal (logical) consequence of the axioms of ZFC, using a finite (or recursively generated) number of inference rules and initial premises.
In other words, when a person finally finds a correct solution of a conjecture, then the result of his/her research can be simulated (just formally) 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 at the beginning one can focus essentially on solvable conjectures, i.e., on problems having an explicit formal proof or counterexample 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. Moreover, after finding initial solutions for the former collections of questions, one can have initial evidence in order to meta-model also the way in which people generate and prove ‘undecidability’ of (some) conjectures.
So, Artificial Mathematical Intelligence deals with the construction (implementation) of a computer program being able to generate a human-style solution of 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 conjectures are clearly important from a purely theoretical perspective, within our AMI meta-project the decidable sentences will have an initial central focus of attention.

So far, we have a considerable amount of significant evidence in favour of AMI. For instance, the co-discovery with the help of programs of the notions of refactorable Numbers, Multiplicative Rings (sometimes known as Containment-Division Rings), the (quasi-)integer and (quasi-)complex numbers and prime ideals (over Dedekind domains). The artificial generation of seminal notions of Fields and Galois Theory like fields, fields extensions, group of automorphisms of a field and meta-Galois Group of a field extension. Furthermore, we have developed and improved software being able to simulate analogy making and conceptual blending in initial mathematical theories. Specifically, we have co-discovered with the help of several computer programs partial axiomatizations of the integers, commutative rings with unity with compatible divisibility relations, and Goldbach rings.

For more specific information regarding the above results, the reader can consult the following webpage: https://dagomez1982.wixsite.com/misitio