License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.9
URN: urn:nbn:de:0030-drops-183846
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18384/
Carneiro, Mario ;
Brown, Chad E. ;
Urban, Josef
Automated Theorem Proving for Metamath
Abstract
Metamath is a proof assistant that keeps surprising outsiders by its combination of a very minimalist design with a large library of advanced results, ranking high on the Freek Wiedijk’s 100 list. In this work, we develop several translations of the Metamath logic and its large set-theoretical library into higher-order and first-order TPTP formats for automated theorem provers (ATPs). We show that state-of-the-art ATPs can prove 68% of the Metamath problems automatically when using the premises that were used in the human-written Metamath proofs. Finally, we add proof reconstruction and premise selection methods and combine the components into the first hammer system for Metamath.
BibTeX - Entry
@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9,
author = {Carneiro, Mario and Brown, Chad E. and Urban, Josef},
title = {{Automated Theorem Proving for Metamath}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18384},
URN = {urn:nbn:de:0030-drops-183846},
doi = {10.4230/LIPIcs.ITP.2023.9},
annote = {Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery}
}
