Elamur Research⌕
☰
home / authors / Cezary Kaliszyk

Cezary Kaliszyk

Cezary Kaliszyk has 2 papers in our library, in 2012–2016, most of them on Reasoning; often with Josef Urban.

2 papers in our library · 2012–2016

OpenAlex · ORCID · Wikidata · h-index 26 · 213 works · 2,490 citations OpenAlex, 2026-10-14

📄 2 works in our library · 🔗 Cited 311 times in our library · 11 more in our library without a page yet · ⭐ Paper Stars ranking: #5010

The profile is the library's match of the name; two people with one name are not always told apart.

Elsewhere: Google Scholar · Semantic Scholar · dblp · ACL Anthology

 Affiliations

🎓Universität InnsbruckInnsbruck · Austria2012–2026 · 135 papersEducation 2012–2016 · Habilitation, Computer ScienceEmployment 2012–2024 · Associate Professor, Informatikcurrent🎓The University of MelbourneMelbourne · Australia2024–2026 · 17 papersEmployment since 2024current🎓Radboud University NijmegenNijmegen · Netherlands2005–2018 · 15 papersEducation 2005–2009 · PhDEmployment 2005–2009🎓University of WarsawWarsaw · Poland2000–2021 · 10 papersEducation 2000–2005 · MSc, Computer ScienceEmployment 2018–2021 · Part time (adjunct), MIMUW🎓University of TsukubaTsukuba · Japan2010–2018 · 4 papersEmployment 2010–2012🎓Technical University of MunichMunich · Germany2009–2011 · 3 papersEmployment 2009–2010🤝International Neurodegenerative Disorders Research CenterPrague · Czechia2023 · 2 papers
🏛️Google BrainMountain View · United States2016Employment 2016 · Faculty Advisor
🏛️Google BrainUnited States2016Employment 2016
🏛️Laboratoire d'Informatique Théorique et AppliquéeMetz · France2005Employment 2005

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 1 more institution on single bylines are not listed.

 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 2 worksArtificial Intelligence · 2 worksComputational Theory and Mathematics · 2 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 2 works

💡 Concepts 1Key ideas and methods explained on our concept pages.Lemma · 2 works

 Works by year

2010s

20161 paper20121 paper

 Papers

The most cited first (OpenAlex and our library).

  1. Learning-Assisted Automated Reasoning with Flyspeck (2012 · 165 citations)
    The paper addresses the lack of a "hammer" for HOL Light: a tool that automatically proves a new goal by choosing relevant lemmas from a large library and handing them to external automated theorem provers (ATPs).
  2. Hammering towards QED (2016 · 127 citations)
    This survey covers "hammers," tools that let users of proof assistants prove hard lemmas automatically. The user does not have to script the proof search by hand. The tools draw on very large formal libraries, and the name comes from Sledgehammer for Isabelle and HOLyHammer for HOL Light.

All works

13 works of theirs in our library, the most cited first; 2 with a page here, the others link their original until we summarise them.

  1. Learning-Assisted Automated Reasoning with FlyspeckarXiv:1211.7012 (J. Automated Reasoninig 54(1): 99, 2014)Cezary Kaliszyk, Josef Urban2012 · 165 citations
  2. Deep Network Guided Proof Search ↗arXiv:1701.06972 (In Thomas Eiter and David Sands, editors, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pages 85-105, EasyChair, 2017. ISSN 2398-7340) · no summary yetSarah Loos et al.2017 · 139 citations
  3. Hammering towards QEDJournal of Formalized Reasoning 9(1)Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, et al.2016 · 127 citations
  4. MizAR 40 for Mizar 40 ↗arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015)) · no summary yetCezary Kaliszyk, Josef Urban2013 · 112 citations
  5. A formal proof of the Kepler conjecture ↗arXiv:1501.02155 · no summary yetThomas Hales et al.2015 · 79 citations
  6. First Experiments with Neural Translation of Informal to Formal Mathematics ↗arXiv:1805.06502 · no summary yetQingxiang Wang, Cezary Kaliszyk, Josef Urban2018 · 66 citations
  7. TacticToe: Learning to Prove with Tactics ↗arXiv:1804.00596 (J. Automated Reasoning 65(2): 257-286, 2021) · no summary yetThibault Gauthier et al.2018 · 57 citations
  8. Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar ↗arXiv:1912.02636 · no summary yetQingxiang Wang et al.2019 · 50 citations
  9. Reinforcement Learning of Theorem Proving ↗arXiv:1805.07563 · no summary yetCezary Kaliszyk et al.2018 · 50 citations
  10. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving ↗arXiv:1703.00426 · no summary yetCezary Kaliszyk, François Chollet, Christian Szegedy2017 · 48 citations
  11. Property Invariant Embedding for Automated Reasoning ↗arXiv:1911.12073 (ECAI 2020 - 24th European Conference on Artificial Intelligence) · no summary yetMiroslav Olšák, Cezary Kaliszyk, Josef Urban2019 · 30 citations
  12. Towards Finding Longer Proofs ↗arXiv:1905.13100 · no summary yetZsolt Zombori et al.2019 · 21 citations
  13. HOL(y)Hammer: Online ATP Service for HOL Light ↗arXiv:1309.4962 · no summary yetCezary Kaliszyk, Josef Urban2013 · 13 citations

 Co-authors here

1 co-author with a page, the most papers together first.

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

 Cited by

Papers of our library cite their works 311 times (of the 149,439 papers whose bibliographies we read); 15 citing papers with a page here →.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/