\input zb-basic
\input zb-matheduc
\iteman{ZMATH 2016f.00796}
\itemau{Hipolito, In\^{e}s}
\itemti{Plato on the foundations of modern theorem provers.}
\itemso{Math. Enthus. 13, No. 3, 303-314 (2016).}
\itemab
Summary: Is it possible to achieve such a proof that is independent of both acts and dispositions of the human mind? Plato is one of the great contributors to the foundations of mathematics. He discussed, 2400 years ago, the importance of clear and precise definitions as fundamental entities in mathematics, independent of the human mind. In the seventh book of his masterpiece, The Republic, Plato states ``arithmetic has a very great and elevating effect, compelling the soul to reason about abstract number, and rebelling against the introduction of visible or tangible objects into the argument". In the light of this thought, I will discuss the status of mathematical entities in the twentieth first century, an era when it is already possible to demonstrate theorems and construct formal axiomatic derivations of remarkable complexity with artificial intelligent agents -- the modern theorem provers.
\itemrv{~}
\itemcc{E50 A30 R40}
\itemut{proving; proofs; history of mathematics; mathematical reasoning; Plato; conception of arithmetic; existence; abstractness; independence; modern theorem provers; formal proofs; computer-assisted proofs; axiomatics; proof assistants; artificial intelligent agents; symbolic language; four-color theorem; Jordan curve theorem; odd-order theorem; formal systems}
\itemli{http://scholarworks.umt.edu/tme/vol13/iss3/8}
\end