---
title: "MizAR 40 for Mizar 40 — paper by Kaliszyk and Urban (2013)"
description: "They then train fast premise-selection methods on proof dependencies taken from earlier proofs… 33 references, cited by 20 papers here."
authors: ["Cezary Kaliszyk", "Josef Urban"]
year: 2013
venue: "arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015))"
source: "https://arxiv.org/abs/1310.2805"
doi: "10.1007/s10817-015-9330-8"
arxiv: "1310.2805"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2013](https://md.research.elamur.ai/free/en/papers/2013/) / MizAR 40 for Mizar 40

# MizAR 40 for Mizar 40

**Authors:** [Cezary Kaliszyk](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) and [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2013 · **Venue:** [arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015))](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/) ([Journal of Automated Reasoning 2013](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://doi.org/10.1007/s10817-015-9330-8) · [PDF](https://arxiv.org/pdf/1310.2805v1) · [DOI 10.1007/s10817-015-9330-8](https://doi.org/10.1007/s10817-015-9330-8) · [arXiv 1310.2805](https://arxiv.org/abs/1310.2805) · [OpenAlex](https://openalex.org/W1815556503)

**Citations:** 92 citations (OpenAlex, 2026-10-14) · [20](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper asks how much of the Mizar Mathematical Library (MML) can be proved fully automatically by learning-guided ATP systems that scale to the whole library rather than to small benchmarks. Building on their earlier Flyspeck/HOL Light work, the authors translate MML 4.181.1147 into TPTP with MPTP. They then train fast premise-selection methods on proof dependencies taken from earlier proofs, using only chronologically preceding proofs. The selected premises are passed to the Vampire, E and Z3 provers. Training data are improved over several MaLARea-style rounds: better selectors yield new proofs, and those proofs become fresh training data. The best result comes from running 14 complementary method/prover combinations in parallel for 30 seconds on a 14-CPU machine, which proves 40.6% of the roughly 58,000 top-level theorems with no user help. Training on the full library takes only 1–3 seconds, so the methods could be deployed in the online MizAR service. This makes automated assistance practical for Mizar users and lowers the barrier to formalizing mathematics.

## Key points
- The corpus is MML 4.181.1147: 57,897 theorems and top-level lemmas, plus about 90,000 other formulas (about 150,000 in total). It is translated via MPTP, and the provers are Vampire 3.0, Z3 4.0 and E 1.8 run with the Epar strategies.
- Six iterative passes increased the number of ATP-proved theorems used for training from 27,842 (48%) to 32,165 (55.6%). Combining human and learned premise selection eventually proved 32,557 theorems (56.2%).
- The premise selectors include:
  - naive Bayes (nb, nb_idf);
  - distance-weighted k-NN with IDF weighting;
  - k-NN on an LSI-reduced feature space built with gensim (800, 3200 and 6,400 topics);
  - recursive dependency weighting (geo_1_F, geo_r_F);
  - rank-combination ensembles, of which comb_min and comb_geo worked best.
- Formulas are described by MaLARea-style syntactic features (symbols, terms, subterms), mostly with all variables renamed to a single variable.
- In MizAR, the selectors are retrained for each query on the whole MML plus the submitted article. To better handle proof-local lemmas, local constants are also generalized to variables when extracting features.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Radboud University Nijmegen](https://md.research.elamur.ai/free/en/universities/radboud-university-nijmegen/) — University, Nijmegen, Netherlands · 26 works · 2,125 citations
- [Universität Innsbruck](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) — University, Innsbruck, Austria · 23 works · 1,475 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Cezary Kaliszyk and Josef Urban. 2013. MizAR 40 for Mizar 40. arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015)).

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{kaliszyk2013mizar,
  title = {{MizAR 40 for Mizar 40}},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2013},
  doi = {10.1007/s10817-015-9330-8},
  eprint = {1310.2805},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1007/s10817-015-9330-8}
}
```

- [← previous Aggregated Word Pair Features for Implicit Discourse Relation Disambiguation](https://md.research.elamur.ai/free/en/papers/biran-2013-aggregated-word-pair-features-implicit/)
- [next → Named Entity Recognition using Cross-lingual Resources: Arabic as an Example](https://md.research.elamur.ai/free/en/papers/darwish-2013-named-entity-recognition-cross-lingual/)
- [↑ back to papers of 2013](https://md.research.elamur.ai/free/en/papers/2013/)

## References

33 references, 4 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. [Premise selection for mathematics by corpus analysis and kernel methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/). Journal of Automated Reasoning, 2013. http://dx.doi.org/10.1007/s10817-013-9286-5. [↗](http://dx.doi.org/10.1007/s10817-013-9286-5)
2. Jesse Alama, Daniel Kühlwein, and Josef Urban. Automated and Human Proofs in General Mathematics: An Initial Comparison. In Nikolaj Bjørner and Andrei Voronkov, editors, LPAR, volume 7180 of LNCS, pages 37–45. Springer, 2012. [find](https://scholar.google.com/scholar?q=Jesse+Alama%2C+Daniel+Ku%CC%88hlwein%2C+and+Josef+Urban%2E+Automated+and+Human+Proofs+in+General+Mathematics%3A+An+Initial+Comparison%2E+In+Nikolaj+Bj%C3%B8rner+and+Andrei+Voronkov%2C+editors%2C+LPAR%2C+volume+7180+of+LNCS%2C+pa)
3. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. [find](https://scholar.google.com/scholar?q=Leonardo+Mendonc%CC%A7a+de+Moura+and+Nikolaj+Bj%C3%B8rner%2E+Z3%3A+An+Efficient+SMT+Solver%2E+In+C%2E+R%2E+Ramakrishnan+and+Jakob+Rehof%2C+editors%2C+TACAS%2C+volume+4963+of+LNCS%2C+pages+337%E2%80%93340%2E+Springer%2C+2008%2E)
4. Scott C. Deerwester, Susan T. Dumais, Thomas K. Landauer, George W. Furnas, and Richard A. Harshman. Indexing by Latent Semantic Analysis. JASIS, 41(6):391–407, 1990. [find](https://scholar.google.com/scholar?q=Scott+C%2E+Deerwester%2C+Susan+T%2E+Dumais%2C+Thomas+K%2E+Landauer%2C+George+W%2E+Furnas%2C+and+Richard+A%2E+Harshman%2E+Indexing+by+Latent+Semantic+Analysis%2E+JASIS%2C+41%286%29%3A391%E2%80%93407%2C+1990%2E)
5. Sahibsingh A. Dudani. The distance-weighted k-nearest-neighbor rule. Systems, Man and Cybernetics, IEEE Transactions on, SMC-6(4):325–327, 1976. [find](https://scholar.google.com/scholar?q=Sahibsingh+A%2E+Dudani%2E+The+distance%2Dweighted+k%2Dnearest%2Dneighbor+rule%2E+Systems%2C+Man+and+Cybernetics%2C+IEEE+Transactions+on%2C+SMC%2D6%284%29%3A325%E2%80%93327%2C+1976%2E)
6. Adam Grabowski, Artur Korni lowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010. [find](https://scholar.google.com/scholar?q=Adam+Grabowski%2C+Artur+Korni+lowicz%2C+and+Adam+Naumowicz%2E+Mizar+in+a+nutshell%2E+Journal+of+Formalized+Reasoning%2C+3%282%29%3A153%E2%80%93245%2C+2010%2E)
7. Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Ger… [find](https://scholar.google.com/scholar?q=Thomas+C%2E+Hales%2E+Introduction+to+the+Flyspeck+project%2E+In+Thierry+Coquand%2C+Henri+Lombardi%2C+and+Marie%2DFranc%CC%A7oise+Roy%2C+editors%2C+Mathematics%2C+Algorithms%2C+Proofs%2C+volume+05021+of+Dagstuhl+Seminar+Proceedi)
8. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, FMCAD, volume 1166 of LNCS, pages 265–269. Springer, 1996. [find](https://scholar.google.com/scholar?q=John+Harrison%2E+HOL+Light%3A+A+tutorial+introduction%2E+In+Mandayam+K%2E+Srivas+and+Albert+John+Camilleri%2C+editors%2C+FMCAD%2C+volume+1166+of+LNCS%2C+pages+265%E2%80%93269%2E+Springer%2C+1996%2E)
9. Krystof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 299–314. Springer, 2011. [find](https://scholar.google.com/scholar?q=Krystof+Hoder+and+Andrei+Voronkov%2E+Sine+qua+non+for+large+theory+reasoning%2E+In+Nikolaj+Bj%C3%B8rner+and+Viorica+Sofronie%2DStokkermans%2C+editors%2C+CADE%2C+volume+6803+of+LNCS%2C+pages+299%E2%80%93314%2E+Springer%2C+2011%2E)
10. Karen Sprck Jones. A statistical interpretation of term specificity and its application in retrieval. Journal of Documentation, 28:11–21, 1972. [find](https://scholar.google.com/scholar?q=Karen+Sprck+Jones%2E+A+statistical+interpretation+of+term+specificity+and+its+application+in+retrieval%2E+Journal+of+Documentation%2C+28%3A11%E2%80%9321%2C+1972%2E)
11. Cezary Kaliszyk and Josef Urban. [Learning-assisted automated reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). CoRR, abs/1211.7012, 2012.
12. Cezary Kaliszyk and Josef Urban. Automated reasoning service for HOL Light. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 120– 135. Springer, 2013. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Automated+reasoning+service+for+HOL+Light%2E+In+Jacques+Carette%2C+David+Aspinall%2C+Christoph+Lange%2C+Petr+Sojka%2C+and+Wolfgang+Windsteiger%2C+editors%2C+MKM%2FCalculemus%2FDML%2C+volu)
13. Cezary Kaliszyk and Josef Urban. [HOL(y)Hammer: Online ATP service for HOL Light](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/). CoRR, abs/1309.4962, 2013.
14. Cezary Kaliszyk and Josef Urban. PRocH: Proof reconstruction for HOL Light. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 267–274. Springer, 2013. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+PRocH%3A+Proof+reconstruction+for+HOL+Light%2E+In+Maria+Paola+Bonacina%2C+editor%2C+CADE%2C+volume+7898+of+Lecture+Notes+in+Computer+Science%2C+pages+267%E2%80%93274%2E+Springer%2C+2013%2E)
15. Cezary Kaliszyk and Josef Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 87–95. EasyChair, 2013. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk+and+Josef+Urban%2E+Stronger+automation+for+Flyspeck+by+feature+weighting+and+strategy+evolution%2E+In+Jasmin+Christian+Blanchette+and+Josef+Urban%2C+editors%2C+PxTP+2013%2C+volume+14+of+EPiC+Ser)
16. Daniel Kuehlwein and Josef Urban. Learning from multiple proofs: First experiments. In Pascal Fontaine, Renate A. Schmidt, and Stephan Schulz, editors, PAAR-2012, volume 21 of EPiC Series, pages 82–94. EasyChair, 2013. [find](https://scholar.google.com/scholar?q=Daniel+Kuehlwein+and+Josef+Urban%2E+Learning+from+multiple+proofs%3A+First+experiments%2E+In+Pascal+Fontaine%2C+Renate+A%2E+Schmidt%2C+and+Stephan+Schulz%2C+editors%2C+PAAR%2D2012%2C+volume+21+of+EPiC+Series%2C+pages+82%E2%80%9394)
17. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP, volume 7998 of Lecture Notes in Computer Science, pages 35–50. Springer, 2013. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Jasmin+Christian+Blanchette%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+MaSh%3A+Machine+learning+for+Sledgehammer%2E+In+Sandrine+Blazy%2C+Christine+Paulin%2DMohring%2C+and+David+Pichardie%2C+editors%2C+ITP)
18. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378–392. Springer, 2012. [find](https://scholar.google.com/scholar?q=Daniel+Ku%CC%88hlwein%2C+Twan+van+Laarhoven%2C+Evgeni+Tsivtsivadze%2C+Josef+Urban%2C+and+Tom+Heskes%2E+Overview+and+evaluation+of+premise+selection+techniques+for+large+theory+mathematics%2E+In+Bernhard+Gramlich%2C+Dale)
19. Radim Řehůřek and Petr Sojka. Software framework for topic modelling with large corpora. In Proceedings of the LREC 2010 Workshop on New Challenges for NLP Frameworks, pages 45–50, Valletta, Malta, May 2010. ELRA. [find](https://scholar.google.com/scholar?q=Radim+R%CC%8Cehu%CC%8Ar%CC%8Cek+and+Petr+Sojka%2E+Software+framework+for+topic+modelling+with+large+corpora%2E+In+Proceedings+of+the+LREC+2010+Workshop+on+New+Challenges+for+NLP+Frameworks%2C+pages+45%E2%80%9350%2C+Valletta%2C+Malta%2C)
20. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. AI Commun., 15(2-3):91–110, 2002. [find](https://scholar.google.com/scholar?q=Alexandre+Riazanov+and+Andrei+Voronkov%2E+The+design+and+implementation+of+VAMPIRE%2E+AI+Commun%2E%2C+15%282%2D3%29%3A91%E2%80%93110%2C+2002%2E)
21. Robert E. Schapire. The strength of weak learnability. Machine Learning, 5:197–227, 1990. [find](https://scholar.google.com/scholar?q=Robert+E%2E+Schapire%2E+The+strength+of+weak+learnability%2E+Machine+Learning%2C+5%3A197%E2%80%93227%2C+1990%2E)
22. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+E+%2D+A+Brainiac+Theorem+Prover%2E+AI+Commun%2E%2C+15%282%2D3%29%3A111%E2%80%93126%2C+2002%2E)
23. John Shawe-Taylor and Nello Cristianini. Kernel Methods for Pattern Analysis. Cambridge University Press, New York, NY, USA, 2004. [find](https://scholar.google.com/scholar?q=John+Shawe%2DTaylor+and+Nello+Cristianini%2E+Kernel+Methods+for+Pattern+Analysis%2E+Cambridge+University+Press%2C+New+York%2C+NY%2C+USA%2C+2004%2E)
24. Steffen Juilf Smolka and Jasmin Christian Blanchette. Robust, semi-intelligible isabelle proofs from atp proofs. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 117–132. EasyChair, 2013. [find](https://scholar.google.com/scholar?q=Steffen+Juilf+Smolka+and+Jasmin+Christian+Blanchette%2E+Robust%2C+semi%2Dintelligible+isabelle+proofs+from+atp+proofs%2E+In+Jasmin+Christian+Blanchette+and+Josef+Urban%2C+editors%2C+PxTP+2013%2C+volume+14+of+EPiC+S)
25. Josef Urban. Translating Mizar for first order theorem provers. In MKM, volume 2594 of LNCS, pages 203–215. Springer, 2003. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+Translating+Mizar+for+first+order+theorem+provers%2E+In+MKM%2C+volume+2594+of+LNCS%2C+pages+203%E2%80%93215%2E+Springer%2C+2003%2E)
26. Josef Urban. MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MPTP+%2D+Motivation%2C+Implementation%2C+First+Experiments%2E+Journal+of+Automated+Reasoning%2C+33%283%2D4%29%3A319%E2%80%93339%2C+2004%2E)
27. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MPTP+0%2E2%3A+Design%2C+implementation%2C+and+initial+experiments%2E+J%2E+Autom%2E+Reasoning%2C+37%281%2D2%29%3A21%E2%80%9343%2C+2006%2E)
28. Josef Urban. [MaLARea: a metasystem for automated reasoning in large theories](https://md.research.elamur.ai/free/en/papers/urban-2007-malarea-metasystem-automated-reasoning-large/). In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, ESARLT, volume 257 of CEUR Workshop Proceedings. CEUR-WS.org, 2007.
29. Josef Urban. An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper). In Peter Höfner, Annabelle McIver, and Georg Struth, editors, ATE Workshop, volume 760 of CEUR Workshop Proceedings, pages 3–8. CEUR-WS.org, 2011. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+An+Overview+of+Methods+for+Large%2DTheory+Automated+Theorem+Proving+%28Invited+Paper%29%2E+In+Peter+Ho%CC%88fner%2C+Annabelle+McIver%2C+and+Georg+Struth%2C+editors%2C+ATE+Workshop%2C+volume+760+of+CEUR+Workshop)
30. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2013. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+BliStr%3A+The+Blind+Strategymaker%2E+CoRR%2C+abs%2F1301%2E2683%2C+2013%2E+%E2%80%94+%5BarXiv%3A1301%2E2683%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1301%2E2683%29)
31. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Piotr+Rudnicki%2C+and+Geoff+Sutcliffe%2E+ATP+and+presentation+service+for+Mizar+formalizations%2E+J%2E+Autom%2E+Reasoning%2C+50%3A229%E2%80%93241%2C+2013%2E)
32. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. [find](https://scholar.google.com/scholar?q=Josef+Urban%2C+Geoff+Sutcliffe%2C+Petr+Pudla%CC%81k%2C+and+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2E+MaLARea+SG1+%2D+Machine+Learner+for+Automated+Reasoning+with+Semantic+Guidance%2E+In+Alessandro+Armando%2C+Peter+Baumgartner%2C+and+Gilles+Dow)
33. Josef Urban and Jiřı́ Vyskočil. Theorem proving in large formal mathematics as an emerging AI field. In Maria Paola Bonacina and Mark E. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William McCune, volume 7788 of LNAI, pages 240–257. Springer, 2013. [find](https://scholar.google.com/scholar?q=Josef+Urban+and+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2E+Theorem+proving+in+large+formal+mathematics+as+an+emerging+AI+field%2E+In+Maria+Paola+Bonacina+and+Mark+E%2E+Stickel%2C+editors%2C+Automated+Reasoning+and+Mathematics%3A+Essays)

*Updated 3 November 2026*