SIE - Intelligent Web Proxy Framework. - Grzegorz Andruszkiewicz; Krzysztof Ciebiera; Marcin Gozdalik; Cezary Kaliszyk; Mateusz Srebrny (ICWE, 2004)

Web Interfaces for Proof Assistants. - Cezary Kaliszyk (UITP@FLoC, 2006)

Cooperative Repositories for Formal Proofs. - Pierre Corbineau; Cezary Kaliszyk (Calculemus/MKM, 2007)

Certified Computer Algebra on Top of an Interactive Theorem Prover. - Cezary Kaliszyk; Freek Wiedijk (Calculemus/MKM, 2007)

Automating Side Conditions in Formalized Partial Functions. - Cezary Kaliszyk (AISC/MKM/Calculemus, 2008)

A Real Semantic Web for Mathematics Deserves a Real Semantics. - Cezary Kaliszyk; Pierre Corbineau; Freek Wiedijk; James McKinna; Herman Geuvers (SemWiki, 2008)

Merging Procedural and Declarative Proof. - Cezary Kaliszyk; Freek Wiedijk (TYPES, 2008)

Computing with Classical Real Numbers. - Cezary Kaliszyk; Russell O'Connor (J. Formaliz. Reason., 2009)

CTP-based programming languages?: considerations about an experimental design. - Florian Haftmann; Cezary Kaliszyk; Walther Neuper (ACM Commun. Comput. Algebra, 2010)

Counting Derangements, Non Bijective Functions and the Birthday Problem. - Cezary Kaliszyk (Formaliz. Math., 2010)

Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. - Cezary Kaliszyk; Henk Barendregt (CPP, 2011)

Proof Assistant Decision Procedures for Formalizing Origami. - Cezary Kaliszyk; Tetsuo Ida (Calculemus/MKM, 2011)

Quotients revisited for Isabelle/HOL. - Cezary Kaliszyk; Christian Urban (SAC, 2011)

Algebraic Analysis of Huzita's Origami Operations and Their Extensions. - Fadoua Ghourabi; Asem Kasem; Cezary Kaliszyk (Automated Deduction in Geometry, 2012)

Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. - Cezary Kaliszyk; Josef Urban (PAAR@IJCAR, 2012)

General Bindings and Alpha-Equivalence in Nominal Isabelle - Christian Urban; Cezary Kaliszyk (Log. Methods Comput. Sci., 2012)

Initial Experiments on Deriving a Complete HOL Simplification Set. - Cezary Kaliszyk; Thomas Sternagel (PxTP@CADE, 2013)

PRocH: Proof Reconstruction for HOL Light. - Cezary Kaliszyk; Josef Urban (CADE, 2013)

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. - Cezary Kaliszyk; Josef Urban (PxTP@CADE, 2013)

Scalable LCF-Style Proof Translation. - Cezary Kaliszyk; Alexander Krauss 001 (ITP, 2013)

MaSh: Machine Learning for Sledgehammer. - Daniel Kühlwein; Jasmin Christian Blanchette; Cezary Kaliszyk; Josef Urban (ITP, 2013)

Communicating Formal Proofs: The Case of Flyspeck. - Carst Tankink; Cezary Kaliszyk; Josef Urban; Herman Geuvers (ITP, 2013)

Lemma Mining over HOL Light. - Cezary Kaliszyk; Josef Urban (LPAR, 2013)

Automated Reasoning Service for HOL Light. - Cezary Kaliszyk; Josef Urban (MKM/Calculemus/DML, 2013)

Formal Mathematics on Display: A Wiki for Flyspeck. - Carst Tankink; Cezary Kaliszyk; Josef Urban; Herman Geuvers (MKM/Calculemus/DML, 2013)

Beagle as a HOL4 external ATP method. - Thibault Gauthier; Cezary Kaliszyk; Chantal Keller; Michael Norrish (PAAR@IJCAR, 2014)

Machine Learner for Automated Reasoning 0.4 and 0.5. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (PAAR@IJCAR, 2014)

Matching Concepts across HOL Libraries. - Thibault Gauthier; Cezary Kaliszyk (CICM, 2014)

Towards Knowledge Management for HOL Light. - Cezary Kaliszyk; Florian Rabe 001 (CICM, 2014)

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil; Herman Geuvers (CICM, 2014)

Wikis and Collaborative Systems for Large Formal Mathematics. - Cezary Kaliszyk; Josef Urban (SWCS (LNCS Volume), 2014)

Machine Learning of Coq Proof Guidance: First Experiments. - Cezary Kaliszyk; Lionel Mamane; Josef Urban (SCSS, 2014)

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. - Sebastiaan J. C. Joosten; Cezary Kaliszyk; Josef Urban (ACL2, 2014)

Learning-Assisted Automated Reasoning with Flyspeck. - Cezary Kaliszyk; Josef Urban (J. Autom. Reason., 2014)

System Description: E.T. 0.1. - Cezary Kaliszyk; Stephan Schulz 001; Josef Urban; Jirí Vyskocil (CADE, 2015)

Premise Selection and External Provers for HOL4. - Thibault Gauthier; Cezary Kaliszyk (CPP, 2015)

Certified Connection Tableaux Proofs for HOL Light and TPTP. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (CPP, 2015)

Random Forests for Premise Selection. - Michael Färber 002; Cezary Kaliszyk (FroCos, 2015)

Lemmatization for Stronger Reasoning in Large Theories. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (FroCos, 2015)

Metis-based Paramodulation Tactic for HOL Light. - Michael Färber 002; Cezary Kaliszyk (GCAI, 2015)

Efficient Semantic Features for Automated Reasoning over Large Theories. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (IJCAI, 2015)

Learning to Parse on Aligned Corpora (Rough Diamond). - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (ITP, 2015)

Sharing HOL4 and HOL Light Proof Knowledge. - Thibault Gauthier; Cezary Kaliszyk (LPAR, 2015)

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. - Cezary Kaliszyk; Josef Urban (LPAR, 2015)

Improving Statistical Linguistic Algorithms for Parsing Mathematics. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (IWIL@LPAR, 2015)

Formalizing Physics: Automation, Presentation and Foundation Issues. - Cezary Kaliszyk; Josef Urban; Umair Siddique; Sanaz Khan Afshar; Cvetan Dunchev; Sofiène Tahar (CICM, 2015)

Efficient Low-Level Connection Tableaux. - Cezary Kaliszyk (TABLEAUX, 2015)

A formal proof of the Kepler conjecture. - Thomas C. Hales; Mark Adams; Gertrud Bauer; Dat Tat Dang; John Harrison 001; Truong Le Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Thang Tat Nguyen; Truong Quang Nguyen; Tobias Nipkow; et al. (CoRR, 2015)

Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. - Cezary Kaliszyk; Josef Urban (J. Autom. Reason., 2015)

MizAR 40 for Mizar 40. - Cezary Kaliszyk; Josef Urban (J. Autom. Reason., 2015)

Learning-assisted theorem proving with millions of lemmas. - Cezary Kaliszyk; Josef Urban (J. Symb. Comput., 2015)

HOL(y)Hammer: Online ATP Service for HOL Light. - Cezary Kaliszyk; Josef Urban (Math. Comput. Sci., 2015)

No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. - Michael Färber 002; Cezary Kaliszyk (PAAR@IJCAR, 2016)

TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. - Cezary Kaliszyk; Geoff Sutcliffe; Florian Rabe 001 (PAAR@IJCAR, 2016)

Initial Experiments with Statistical Conjecturing over Large Formal Corpora. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

A Standard for Aligning Mathematical Concepts. - Cezary Kaliszyk; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001 (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Towards a mizar environment for isabelle: foundations and language. - Cezary Kaliszyk; Karol Pak; Josef Urban (CPP, 2016)

Towards Formal Proof Metrics. - David Aspinall 001; Cezary Kaliszyk (FASE, 2016)

What's in a Theorem Name? - David Aspinall 001; Cezary Kaliszyk (ITP, 2016)

Goal Translation for a Hammer for Coq (Extended Abstract). - Lukasz Czajka 001; Cezary Kaliszyk (HaTT@IJCAR, 2016)

Monte Carlo Connection Prover. - Michael Färber 002; Cezary Kaliszyk; Josef Urban (CoRR, 2016)

Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (CoRR, 2016)

A Learning-Based Fact Selector for Isabelle/HOL. - Jasmin Christian Blanchette; David Greenaway; Cezary Kaliszyk; Daniel Kühlwein; Josef Urban (J. Autom. Reason., 2016)

Hammering towards QED. - Jasmin Christian Blanchette; Cezary Kaliszyk; Lawrence C. Paulson; Josef Urban (J. Formaliz. Reason., 2016)

Monte Carlo Tableau Proof Search. - Michael Färber 002; Cezary Kaliszyk; Josef Urban (CADE, 2017)

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle. - Cezary Kaliszyk; Karol Pak (FedCSIS, 2017)

HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. - Cezary Kaliszyk; François Chollet; Christian Szegedy (ICLR (Poster), 2017)

Automating Formalization by Statistical and Semantic Parsing of Mathematics. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (ITP, 2017)

TacticToe: Learning to Reason with HOL4 Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (LPAR, 2017)

Deep Network Guided Proof Search. - Sarah M. Loos; Geoffrey Irving; Christian Szegedy; Cezary Kaliszyk (LPAR, 2017)

Isabelle Formalization of Set Theoretic Structures and Set Comprehensions. - Cezary Kaliszyk; Karol Pak (MACIS, 2017)

Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. - Cezary Kaliszyk; Karol Pak (CICM, 2017)

Classification of Alignments Between Concepts of Formal Mathematical Systems. - Dennis Müller 001; Thibault Gauthier; Cezary Kaliszyk; Michael Kohlhase; Florian Rabe 001 (CICM, 2017)

System Description: Statistical Parsing of Informalized Mizar Formulas. - Cezary Kaliszyk; Josef Urban; Jirí Vyskocil (SYNASC, 2017)

Microeconomics and the First Welfare Theorem. - Julian Parsert; Cezary Kaliszyk (Arch. Formal Proofs, 2017)

Formal microeconomic foundations and the first welfare theorem. - Cezary Kaliszyk; Julian Parsert (CPP, 2018)

Towards a Unified Ordering for Superposition-Based Automated Reasoning. - Jan Jakubuv; Cezary Kaliszyk (ICMS, 2018)

Towards Formal Foundations for Game Theory. - Julian Parsert; Cezary Kaliszyk (ITP, 2018)

Concrete Semantics with Coq and CoqHammer. - Lukasz Czajka 001; Burak Ekici; Cezary Kaliszyk (CICM, 2018)

Isabelle Import Infrastructure for the Mizar Mathematical Library. - Cezary Kaliszyk; Karol Pak (CICM, 2018)

First Experiments with Neural Translation of Informal to Formal Mathematics. - Qingxiang Wang; Cezary Kaliszyk; Josef Urban (CICM, 2018)

Reinforcement Learning of Theorem Proving. - Cezary Kaliszyk; Josef Urban; Henryk Michalewski; Miroslav Olsák (NeurIPS, 2018)

Von-Neumann-Morgenstern Utility Theorem. - Julian Parsert; Cezary Kaliszyk (Arch. Formal Proofs, 2018)

Foreword to the Special Issue on Automated Reasoning. - Pascal Fontaine; Cezary Kaliszyk; Stephan Schulz 001; Josef Urban (AI Commun., 2018)

Learning to Reason with HOL4 tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (CoRR, 2018)

Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (CoRR, 2018)

Machine Learning Guidance and Proof Certification for Connection Tableaux. - Michael Färber 002; Cezary Kaliszyk; Josef Urban (CoRR, 2018)

Hammer for Coq: Automation for Dependent Type Theory. - Lukasz Czajka 001; Cezary Kaliszyk (J. Autom. Reason., 2018)

GRUNGE: A Grand Unified ATP Challenge. - Chad E. Brown; Thibault Gauthier; Cezary Kaliszyk; Geoff Sutcliffe; Josef Urban (CADE, 2019)

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. - Chad E. Brown; Cezary Kaliszyk; Karol Pak (ITP, 2019)

Declarative Proof Translation (Short Paper). - Cezary Kaliszyk; Karol Pak (ITP, 2019)

Certification of Nonclausal Connection Tableaux Proofs. - Michael Färber 002; Cezary Kaliszyk (TABLEAUX, 2019)

Linear Programming. - Julian Parsert; Cezary Kaliszyk (Arch. Formal Proofs, 2019)

Can Neural Networks Learn Symbolic Rewriting? - Bartosz Piotrowski; Josef Urban; Chad E. Brown; Cezary Kaliszyk (CoRR, 2019)

Semantics of Mizar as an Isabelle Object Logic. - Cezary Kaliszyk; Karol Pak (J. Autom. Reason., 2019)

Aligning concepts across proof assistant libraries. - Thibault Gauthier; Cezary Kaliszyk (J. Symb. Comput., 2019)

Exploration of neural machine translation in autoformalization of mathematics in Mizar. - Qingxiang Wang; Chad E. Brown; Cezary Kaliszyk; Josef Urban (CPP, 2020)

Property Invariant Embedding for Automated Reasoning. - Miroslav Olsák; Cezary Kaliszyk; Josef Urban (ECAI, 2020)

Property Preserving Embedding of First-order Logic. - Julian Parsert; Stephanie Autherith; Cezary Kaliszyk (GCAI, 2020)

A Survey of Languages for Formalizing Mathematics. - Cezary Kaliszyk; Florian Rabe 001 (CICM, 2020)

Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. - Burak Ekici; Cezary Kaliszyk (Math. Comput. Sci., 2020)

Relaxed Weighted Path Order in Theorem Proving. - Jan Jakubuv; Cezary Kaliszyk (Math. Comput. Sci., 2020)

JEFL: Joint Embedding of Formal Proof Libraries. - Qingxiang Wang; Cezary Kaliszyk (FroCoS, 2021)

Disambiguating Symbolic Expressions in Informal Documents. - Dennis Müller 001; Cezary Kaliszyk (ICLR, 2021)

Online Machine Learning Techniques for Coq: A Comparison. - Liao Zhang; Lasse Blaauwbroek; Bartosz Piotrowski; Prokop Cerný; Cezary Kaliszyk; Josef Urban (CICM, 2021)

Towards Finding Longer Proofs. - Zsolt Zombori; Adrián Csiszárik; Henryk Michalewski; Cezary Kaliszyk; Josef Urban (TABLEAUX, 2021)

A Study of Continuous Vector Representationsfor Theorem Proving. - Stanislaw J. Purgal; Julian Parsert; Cezary Kaliszyk (CoRR, 2021)

Learning Higher-Order Programs without Meta-Interpretive Learning. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (CoRR, 2021)

Machine Learning Guidance for Connection Tableaux. - Michael Färber 002; Cezary Kaliszyk; Josef Urban (J. Autom. Reason., 2021)

TacticToe: Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (J. Autom. Reason., 2021)

A study of continuous vector representations for theorem proving. - Stanislaw J. Purgal; Julian Parsert; Cezary Kaliszyk (J. Log. Comput., 2021)

Lash 1.0 (System Description). - Chad E. Brown; Cezary Kaliszyk (IJCAR, 2022)

Proofgold: Blockchain for Formal Methods. - Chad E. Brown; Cezary Kaliszyk; Thibault Gauthier; Josef Urban (FMBC@CAV, 2022)

Adversarial Learning to Reason in an Arbitrary Logic. - Stanislaw J. Purgal; Cezary Kaliszyk (FLAIRS, 2022)

Learning Higher-Order Logic Programs From Failures. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (IJCAI, 2022)

The Isabelle ENIGMA. - Zarathustra Amadeus Goertzel; Jan Jakubuv; Cezary Kaliszyk; Miroslav Olsák; Jelle Piepenbrock; Josef Urban (ITP, 2022)

Formalizing a Diophantine Representation of the Set of Prime Numbers. - Karol Pak; Cezary Kaliszyk (ITP, 2022)

Lazy Paramodulation in Practice. - Grzegorz Prusak; Cezary Kaliszyk (PAAR@IJCAR, 2022)

Abstract: Challenges and Solutions for Higher-Order SMT Proofs. - Chad E. Brown; Mikolás Janota; Cezary Kaliszyk (SMT, 2022)

Differentiable Inductive Logic Programming in High-Dimensional Space. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (CoRR, 2022)

Improved Assistance for Interactive Proof (Keynote). - Cezary Kaliszyk (CPP, 2023)

Learning Proof Transformations and Its Applications in Interactive Theorem Proving. - Liao Zhang; Lasse Blaauwbroek; Cezary Kaliszyk; Josef Urban (FroCoS, 2023)

MizAR 60 for Mizar 50. - Jan Jakubuv; Karel Chvalovský; Zarathustra Amadeus Goertzel; Cezary Kaliszyk; Mirek Olsák; Bartosz Piotrowski; Stephan Schulz 001; Martin Suda 001; Josef Urban (ITP, 2023)

Experiments on Infinite Model Finding in SMT Solving. - Julian Parsert; Chad E. Brown; Mikolas Janota; Cezary Kaliszyk (LPAR, 2023)

VizAR: Visualization of Automated Reasoning Proofs (System Description). - Jan Jakubuv; Cezary Kaliszyk (CICM, 2023)

Combining Higher-Order Logic with Set Theory Formalizations. - Cezary Kaliszyk; Karol Pak (J. Autom. Reason., 2023)

Learning Guided Automated Reasoning: A Brief Survey. - Lasse Blaauwbroek; David M. Cerna; Thibault Gauthier; Jan Jakubuv; Cezary Kaliszyk; Martin Suda 001; Josef Urban (Logics and Type Systems in Theory and Practice, 2024)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (IJCAR (1), 2024)

Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. - Karol Pak; Cezary Kaliszyk (ITP, 2024)

Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery. - Kristina Aleksandrova; Jan Jakubuv; Cezary Kaliszyk (LPAR, 2024)

Experiments with Choice in Dependently-Typed Higher-Order Logic. - Daniel Ranalter; Chad E. Brown; Cezary Kaliszyk (LPAR, 2024)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version). - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (CoRR, 2024)

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction. - Liao Zhang; David M. Cerna; Cezary Kaliszyk (CoRR, 2024)

Automated Strategy Invention for Confluence of Term Rewrite Systems. - Liao Zhang; Fabian Mitterwallner; Jan Jakubuv; Cezary Kaliszyk (CoRR, 2024)

The Dependently Typed Higher-Order Form for the TPTP World. - Daniel Ranalter; Cezary Kaliszyk; Florian Rabe 001; Geoff Sutcliffe (CoRR, 2025)