| 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 |
| Property invariant embedding for automated reasoning | 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 |
| Computing with classical real numbers | 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 |
