Metamath Zero: Designing a Theorem Prover Prover

Metamath Zero ist ein Verifikationssystem, das auf Einfachheit der Logik und Implementierung abzielt, ohne Kompromisse bei der Effizienz der Verifikation einzugehen. Es wird formell in seiner eigenen Sprache spezifiziert und unterstützt eine Reihe von Übersetzungen in und aus anderen Korrektursprachen. Dieser Aufsatz beschreibt die abstrakte Logik von Metamath Zero, im Wesentlichen eine mehrsortierte Logik erster Ordnung, sowie das binäre Korrekturformat und die Art und Weise, wie es im Wesentlichen eine lineare Zeitverifikation sicherstellen kann, während es im Maßstab dennoch präzise und effizient ist. Metamath Zero hält derzeit den Rekord für die schnellste Verifikation des Satzes. mm Metamath Bibliothek von Beweisen in ZFC (einschließlich 71 der 100 Formalisierungsziele von Wiedijk), bei weniger als 200 ms. Letztlich beabsichtigen wir, es zu verwenden, um die Richtigkeit der Implementierung des Korrekturprüfers bis hin zur binären Ausführbarkeit zu verifizieren, sodass es als Wurzel des Vertrauens für komplexere Beweissysteme verwendet werden kann.