Lean4Lean: Eine formalisierte Metatheorie für den Lean-Theorembeweiser

In dieser Arbeit präsentieren wir einen neuen "externen Verifizierer" für den Lean-Theorembeweiser, der in Lean selbst geschrieben ist. Dies ist der erste vollständige Verifizierer für Lean 4 neben der Referenzimplementierung in C++, die von Lean selbst verwendet wird. Unser neuer Verifizierer ist mit dem Original konkurrenzfähig und kann die gesamte Lean-Mathlib-Bibliothek verifizieren. Darüber hinaus ist es möglich, Eigenschaften über den Kernel selbst auszusagen und zu beweisen, da der Verifizierer in einer Sprache geschrieben ist, die formale Verifikation zulässt.