MizAR 60 for Mizar 50

Jakubův, Jan; Chvalovský, Karel; Goertzel, Zarathustra; Kaliszyk, Cezary; Olšák, Mirek; Piotrowski, Bartosz; Schulz, Stephan; Suda, Martin · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2023

Resource page

Quick overview. Review the resource’s basic details, then access the content using the main button. This page shows only the information needed to identify, cite, and open the work.

Author / responsible party

Jakubův, Jan; Chvalovský, Karel; Goertzel, Zarathustra; Kaliszyk, Cezary; Olšák, Mirek; Piotrowski, Bartosz; Schulz, Stephan; Suda, Martin

Publisher

DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Year

2023

Language

English

Resource access

Open the content from the main option or choose another available source.

OpenAlex OpenAlex Works

Entrar por OpenAlex

Main access

Resource page

Resource reference page. Full text availability has not been automatically confirmed.

Open resource

Summary

Descripción general del contenido del recurso.

As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.

How to cite

Elegí el formato que necesitás y copiá la referencia al portapapeles.

APA 7

Jakubův, J, Chvalovský, K, Goertzel, Z, Kaliszyk, C, Olšák, M, Piotrowski, B, Schulz, S, & Suda, M. (2023). MizAR 60 for Mizar 50. DROPS (Schloss Dagstuhl – Leibniz Center for Informatics). https://doi.org/10.4230/lipics.itp.2023.19

MLA

Jakubův, Jan, et al. MizAR 60 for Mizar 50. DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 2023. https://doi.org/10.4230/lipics.itp.2023.19.

Chicago

Jakubův, Jan, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, and Martin Suda. 2023. MizAR 60 for Mizar 50. DROPS (Schloss Dagstuhl – Leibniz Center for Informatics). https://doi.org/10.4230/lipics.itp.2023.19.

Harvard

Jakubův, J. et al. 2023, MizAR 60 for Mizar 50, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), available at: https://doi.org/10.4230/lipics.itp.2023.19 [Accessed 7 Aug. 2026].

Share and print

Save the record, copy its permanent link, or print it as a PDF.

Export reference

You can export the record in common formats for use in a reference manager.

RIS BibTeX

Resource details

Bibliographic information to help confirm that this is the correct material.

Title: MizAR 60 for Mizar 50

Author / contributors: Jakubův, Jan; Chvalovský, Karel; Goertzel, Zarathustra; Kaliszyk, Cezary; Olšák, Mirek; Piotrowski, Bartosz; Schulz, Stephan; Suda, Martin

Publisher: DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

Publication year: 2023

Language: English

Subjects

Explore related resources through these subjects.

Computer science; Machine translation; Transformer; BLEU; Encoder; Artificial intelligence; Parallelizable manifold; Parsing; Natural language processing; Decoding methods; Language model; Task (project management)