Artificial Mathematical Intelligence, (standard) Automated Reasoning and Technical Computing

At its very beginning, the research field of automated reasoning (or, sometimes called computational logic) has as part of its central global motivations the construction of software being able to generate (and implicitly to solve) concrete mathematical works like for example Whitehead and Russell’s Principia Mathematica [28], [33]; elementary plane euclidean geometry [12], (some parts of) Newton’s Principia [9] and, of course, a lot of instances of propositional calculus [3], among (a few) others. On the other hand, (only) some specific mathematical challenges as the four color’s problem, the Kepler’s theorem and the Feit-Thomsom theorem have giving (significant) additional inspiration for developing more sophisticated (automated) theorem provers [16], [19], [17].

However, apart from a quite reduced number of exceptional formal treatises and outstanding (math- ematical) problems, there has been no global multi- and interdisciplinary effort for developing (interac- tive) theorem provers having as a seminal basis, on the one hand, the most outstanding formalizations of the fundamental cognitive mechanisms used by the mind during mathematical creation-invention [8], [14], [13], [32], [24], [15] together with the most relevant tools that automated reasoning can offer in this direction [31]. And, on the other hand, doing a meta-analysis of dozens of specific mathematical proofs coming from several mathematical domains like real and complex analysis [21], [30]; (abstract and commutative) algebra [10], [7]; differential and algebraic geometry [23], [18], [20]; (algebraic) topology [26], [27]; graph theory [4]; (algebraic and analytic) number theory [22], [1], among others.

So, the Artificial Mathematical Intelligence meta-project (AMI) aim to fill this gap between what we could call ’abstract proof theory’ (as a part of automated reasoning) and ’actual proof theory’ (the actual demonstrations produced by working mathematicians in daily research).

Thus, with the former considerations in mind and regarding the role that (current) automated reason- ing can play within AMI, we will direct our main focus of attention to the identification and subsequent refinement of those A. R. techniques which simulate well syntactically and semantically the actual way in which mathematics are done. For instance, the well-known classic technique of skolemization and the cognitive mechanism of (functional) conceptual substratum seem to have structural relations for first-order frameworks [29], [15]. Similarly, one can develop more cognitive-inspired and equally

powerful versions of the sequent calculus with the inspiration of initial formalizations of the conceptual substratum ability [5], [15, §3].

On the other hand, just to mention one framework not so intimately related with a cognitively- inspired model of mathematical invention, we can say that techniques coming from resolution theorem proving seem to have a slightly different motivation and orientation which emerges more from the need

of finding efficient methods in proof verification and proof generation [31, Ch. 2]. Now, at this point it is

worth to mention that the notions of algorithmic complexity and efficiency are conceived with different ’eyes’ within the AMI consortium. Explicitly, one of the main goals of the AMI-software will be to produce

completely detailed and gradually explainable solutions to formal (domain-specific) mathematical

problems, which would take less time to be found that the time required by a professional researcher

(in mathematics or related areas).

So, for example, the AMI-software naturally would require some months of full work for solving a Ph.D.-level mathematical problem, which turns tobe fine in comparison with the standard time that a Ph.D. thesis takes to be done (e.g. three-four years).Finally, nowadays we have on the market several kinds of computer programs which can assist he researcher in mathematics (and related areas) on different tasks (but always in a relatively small collection of mathematical areas) like numerical and symbolic computation, the drawing of technical graphics, solving particular classes of systems of equations, inequalities, Diophantine and differential equations and quantifier elimination; among others [34], [25], [6] (for a more general list see [2]).

On the other hand, other kinds of outstanding software are used for finding proofs in several classes of propositional calculi and for proof verification and proof generation in some specific logics which, in principle, not cover the scope of the mathematics done every day not only by professional mathematician but also for researcher working in related fields, [3], [31]. Furthermore, the last kind of software mentioned before possess, in general, a so highly technical syntax that for the (pure) mathematician (or related researcher) is it not so straightforward starting to use it on his/her daily work, because it wouldr equired months (and sometimes) years of regular study of its main semantic and syntactic features.

There are also a third kind of valuable programs aiming to produce human-style proofs, but in very particular kinds of problems within quite specific theories, e.g. metric space theory (see [11] and the references there).

Now, the AMI meta-project is the first general inter- and intra-disciplinary scientific program aiming to construct a user-friendly formal conjecture-solver interactive software being able not only to find correct solutions of (solvable) mathematical conjectures, but also to offer cognitively-inspired proofs/counterexamples for them. So, a methodological basic difference between the AMI-approach and the former ones, is that we are interested in an artificial simulation of the way in which the re-searcher’s mind tackles a particular conjecture, instead of finding a purely theoretical (and sometimes too technically encoded) solution/verification of it.

REFERENCES

[1] Apostol, T. M. (2013). Introduction to analytic number theory. Springer Science & Business Media. [2] Biere, A., Heule, M., and van Maaren, H. (2009). Handbook of satisfiability, volume 185. IOS press. [3] Bondy, J. A. and Murty, U. S. R. (1976). Graph theory with applications, volume 290. Macmillan London. [4] Buss, S. R. (1998). An introduction to proof theory. Handbook of proof theory, in Studies in Logic and the Foundations of Mathematics, 137:1–78. [5] Char, B. W., Geddes, K. O., Gonnet, G. H., Leong, B. L., Monagan, M. B., and Watt, S. (2013). Maple V library reference manual. Springer Science & Business Media. [6] Eisenbud, D. (1995). Commutative Algebra with a View Toward Algebraic Geometry. Springer- Verlag. [7] Fauconnier, G. and Turner, M. (2003). The Way We Think. Basic Books. [8] Fleuriot, J. D. and Paulson, L. C. (1998). A combination of nonstandard analysis and geometry theorem proving, with application to newton’s principia. In International Conference on Automated Deduction, pages 3–16. Springer. [9] Fraleigh, J. B. (2003). A first course in abstract algebra. Pearson Education India. [10] Ganesalingam, M. and Gowers, W. T. (2016). A fully automatic theorem prover with human-style output. Journal of Automated Reasoning, pages 1–39. [11] Gelernter, H. (1959). Realization of a geometry theorem proving machine. In IFIP Congress, pages 273–281. [12] Goguen, J. (1999). An introduction to algebraic semiotic with application to user interface design. In Computation for methaphors, analogy and agents. C. L. Nehaniv, Ed. Vol. 1562, pages 242–291. [13] Goguen, J. (Keio University Press, 2001). Mathematical models of cognitive space and time. Proceedings of the Interdisciplinary Conference on Reasoning and Cognition, 123:125–148. [14] Gomez-Ramirez, D. A. J. and Hetzl, S. Functional conceptual substratum as a new cognitive mechanism for mathematical creation. Arxiv. [15] Gonthier, G. (2008). Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393. [16] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., OConnor, R., Biha, S. O., et al. (2013). A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving, pages 163–179. Springer. [17] Grothendieck, A. and Dieudonné, J. (1971). Eléments de Géométrie Algébrique I. Springer. [18] Hales, T. C. (2005). A proof of the kepler conjecture. Annals of mathematics, 162(3):1065–1185. [19] Hartshorne, R. (1977). Algebraic Geometry, volume 52. Springer, New York. [20] Hewitt, E. and Stromberg, K. (2013). Real and abstract analysis: a modern treatment of the theory of functions of a real variable. Springer-Verlag. [21] Janusz, G. J. (1996). Algebraic number fields, volume 7. American Mathematical Soc. [22] Kobayashi, S. and Nomizu, K. (1969). Foundations of differential geometry, volume 2. Inter- science publishers New York. [23] Lakoff, G. and Núñez, R. E. (2000). Where mathematics comes from: How the embodied mind brings mathematics into being. AMC, 10:12. [24] MatLab, M. (2012). The language of technical computing. The MathWorks, Inc. http://www. mathworks. com. [25] Munkres, J. (2000). Topology. Second Edition. Prentice Hall, Inc.

[26] Munkres, J. R. (1984). Elements of algebraic topology, volume 2. Addison-Wesley Menlo Park.

[27] Newell, A., Shaw, J., and Simon, H. (1957). Empirical explorations with the logic theory machine:A case study in heuristics. Automation of reasoning, 1:1957–1966.

[28] Nonnengart, A. and Weidenbach, C. (2001). Computing small clause normal forms. Handbook ofautomated reasoning, 1(335-367):3.

[29] Palka, B. P. (1991). An introduction to complex function theory. Springer Science & Business.

[30] Robinson, A. J. and Voronkov, A. (2001). Handbook of automated reasoning, volume 1. Elsevier.

[31] Schwering, A., Krumnack, U., Kühnberger, K.-U., and Gust, H. (2009). Syntactic principles ofheuristic driven theory projection. Cognitive Systems Research, 10(3):251–269.

[32] Wang, H. (1960). Toward mechanical mathematics. IBM Journal of research and development,4(1):2–22.

[33] Wikipedia, A. (2017). List of computer algebra systems. https://en.wikipedia.org/wiki/List_of_computer_algebra_systems.

[34] Wolfram, S. (2015). The mathematica book, wolfram media, 2003. Received: November, 2.