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 www.ArtificialMathematicalIntelligence.com