Abstract
First-order translations of large mathematical repositories allow discovery of new proofs by automated reasoning systems. Large amounts of available mathematical knowledge can be re-used by combined AI/ATP systems, possibly in unexpected ways. But automated systems can be also more easily misled by irrelevant knowledge in this setting, and finding deeper proofs is typically more difficult. Both large-theory AI/ATP methods, and translation and data-mining techniques of large formal corpora, have significantly developed recently, providing enough data for an initial comparison of the proofs written by mathematicians and the proofs found automatically. This paper describes such an initial experiment and comparison conducted over the 50000 mathematical theorems from the Mizar Mathematical Library. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Alama, J., Kühlwein, D., & Urban, J. (2012). Automated and human proofs in general mathematics: An initial comparison. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 37–45). https://doi.org/10.1007/978-3-642-28717-6_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
