Wednesday 11 January 2023, 13:00, room 1Z53 and online: From Metamath to Dedukti, and beyond!, Amélie Ledein (Deducteam).

In recent years, the number of proof assistants, automatic provers and proof checkers has steadily increased. One of them, the Dedukti logic framework, aims at making these formal tools interoperable, i.e. making it possible to reuse proofs from tool A in tool B. Another formal tool, Metamath, has the distinction of being in 4th place in the list of systems with the highest number of proofs among Freek Wiedijk's list of 100 theorems to be proved, while consisting of very few features: no dependent type, no polymorphism, and no notion of universes. In order to increase the number of proofs that can be translated into Dedukti, this seminar presents an automatic translator from Metamath to Dedukti. As this translator can use two different encodings of Metamath to Dedukti, I will discuss the advantages and disadvantages from an interoperability point of view. For the Deducteam members, this seminar is an opportunity to discover the new Dedukti translator of the year 2022. For LMF members, this seminar is an opportunity to discover or rediscover how Dedukti translators are designed.