| Publication | Date of Publication | Type |
|---|
| Mizar 60 for Mizar 50 | 2024-11-26 | Paper |
| Initial experiments with TPTP-style automated theorem provers on ACL2 problems | 2024-08-19 | Paper |
| The Isabelle ENIGMA | 2024-07-15 | Paper |
| Formalizing a Diophantine representation of the set of prime numbers | 2024-07-15 | Paper |
| Learning Proof Transformations and Its Applications in Interactive Theorem Proving | 2024-05-03 | Paper |
| VizAR: visualization of automated reasoning proofs (system description) | 2024-02-28 | Paper |
| Combining higher-order logic with set theory formalizations | 2023-06-27 | Paper |
| Declarative Proof Translation (Short Paper) | 2023-02-03 | Paper |
| Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | 2023-02-03 | Paper |
| Lash 1.0 (system description) | 2022-12-07 | Paper |
| Towards finding longer proofs | 2022-05-25 | Paper |
| Formalizing a Diophantine Representation of the Set of Prime Numbers | 2022-04-26 | Paper |
| Online machine learning techniques for Coq: a comparison | 2022-04-22 | Paper |
| JEFL: joint embedding of formal proof libraries | 2022-03-24 | Paper |
| A study of continuous vector representations for theorem proving | 2022-01-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4999300 | 2021-07-06 | Paper |
| TacticToe: learning to prove with tactics | 2021-06-09 | Paper |
| Machine learning guidance for connection tableaux | 2021-06-09 | Paper |
| A survey of languages for formalizing mathematics | 2021-01-20 | Paper |
| Mac Lane's comparison theorem for the Kleisli construction formalized in Coq | 2020-10-30 | Paper |
| Relaxed weighted path order in theorem proving | 2020-10-30 | Paper |
| Certification of nonclausal connection tableaux proofs | 2020-05-14 | Paper |
| GRUNGE: a grand unified ATP challenge | 2020-03-10 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
| Semantics of Mizar as an Isabelle object logic | 2019-09-02 | Paper |
| Isabelle Formalization of Set Theoretic Structures and Set Comprehensions | 2019-03-14 | Paper |
| TacticToe: Learning to Reason with HOL4 Tactics | 2019-01-10 | Paper |
| Deep Network Guided Proof Search | 2019-01-10 | Paper |
| Concrete semantics with Coq and CoqHammer | 2018-10-18 | Paper |
| Isabelle import infrastructure for the Mizar Mathematical Library | 2018-10-18 | Paper |
| First experiments with neural translation of informal to formal mathematics | 2018-10-18 | Paper |
| Towards formal foundations for game theory | 2018-10-04 | Paper |
| Hammer for Coq: automation for dependent type theory | 2018-08-21 | Paper |
| Towards a unified ordering for superposition-based automated reasoning | 2018-08-17 | Paper |
| Aligning concepts across proof assistant libraries | 2018-06-14 | Paper |
| Automating formalization by statistical and semantic parsing of mathematics | 2018-01-04 | Paper |
| Monte Carlo tableau proof search | 2017-09-22 | Paper |
| Classification of alignments between concepts of formal mathematical systems | 2017-07-21 | Paper |
| Presentation and manipulation of Mizar properties in an Isabelle object logic | 2017-07-21 | Paper |
| Lemmatization for Stronger Reasoning in Large Theories | 2017-02-27 | Paper |
| Random Forests for Premise Selection | 2017-02-27 | Paper |
| A learning-based fact selector for Isabelle/HOL | 2016-10-27 | Paper |
| What’s in a Theorem Name? | 2016-10-27 | Paper |
| MizAR 40 for Mizar 40 | 2016-05-26 | Paper |
| FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover | 2016-01-12 | Paper |
| Sharing HOL4 and HOL Light Proof Knowledge | 2016-01-12 | Paper |
| Efficient Low-Level Connection Tableaux | 2015-12-11 | Paper |
| System Description: E.T. 0.1 | 2015-12-02 | Paper |
| Formalizing Physics: Automation, Presentation and Foundation Issues | 2015-11-20 | Paper |
| Learning to Parse on Aligned Corpora (Rough Diamond) | 2015-09-14 | Paper |
| Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) | 2015-07-02 | Paper |
| Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) | 2015-06-23 | Paper |
| HOL(y)Hammer: online ATP service for HOL Light | 2015-03-25 | Paper |
| Learning-assisted theorem proving with millions of lemmas | 2015-01-14 | Paper |
| Towards Knowledge Management for HOL Light | 2014-08-07 | Paper |
| Matching Concepts across HOL Libraries | 2014-08-07 | Paper |
| Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description | 2014-08-07 | Paper |
| Lemma Mining over HOL Light | 2014-01-17 | Paper |
| Web interfaces for proof assistants | 2013-12-20 | Paper |
| Algebraic Analysis of Huzita’s Origami Operations and Their Extensions | 2013-09-20 | Paper |
| Automated Reasoning Service for HOL Light | 2013-08-09 | Paper |
| Formal Mathematics on Display: A Wiki for Flyspeck | 2013-08-09 | Paper |
| Communicating Formal Proofs: The Case of Flyspeck | 2013-08-07 | Paper |
| MaSh: Machine Learning for Sledgehammer | 2013-08-07 | Paper |
| Scalable LCF-Style Proof Translation | 2013-08-07 | Paper |
| PRocH: Proof Reconstruction for HOL Light | 2013-06-14 | Paper |
| General bindings and alpha-equivalence in Nominal Isabelle | 2012-07-03 | Paper |
| Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem | 2011-11-22 | Paper |
| Proof Assistant Decision Procedures for Formalizing Origami | 2011-07-29 | Paper |
| General Bindings and Alpha-Equivalence in Nominal Isabelle | 2011-05-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3184782 | 2009-10-22 | Paper |
| Merging Procedural and Declarative Proof | 2009-07-02 | Paper |
| Automating Side Conditions in Formalized Partial Functions | 2009-01-27 | Paper |
| Certified Computer Algebra on Top of an Interactive Theorem Prover | 2007-11-28 | Paper |
| Cooperative Repositories for Formal Proofs | 2007-11-28 | Paper |
