| Publication | Date of Publication | Type |
|---|
| The dependently typed higher-order form for the TPTP world | 2026-02-26 | Paper |
| Exploring formal math on the blockchain: an explorer for Proofgold | 2026-02-19 | Paper |
| Hammering higher order set theory | 2026-02-19 | Paper |
| Conway normal form: bridging approaches for comprehensive formalization of surreal numbers | 2026-02-10 | Paper |
| Experiments with choice in dependently-typed higher-order logic | 2025-02-19 | Paper |
| Experiments on infinite model finding in SMT solving | 2025-02-19 | Paper |
| Learning guided automated reasoning: a brief survey | 2025-02-07 | Paper |
| Tableaux for automated reasoning in dependently-typed higher-order logic | 2025-01-31 | Paper |
| 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)
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Combining higher-order logic with set theory formalizations
Journal of Automated Reasoning | 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)
(available as arXiv preprint) | 2022-12-07 | Paper |
Towards finding longer proofs
(available as arXiv preprint) | 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
(available as arXiv preprint) | 2022-04-22 | Paper |
JEFL: joint embedding of formal proof libraries
(available as arXiv preprint) | 2022-03-24 | Paper |
A study of continuous vector representations for theorem proving
Journal Of Logic And Computation | 2022-01-03 | Paper |
Property invariant embedding for automated reasoning
(available as arXiv preprint) | 2021-07-06 | Paper |
TacticToe: learning to prove with tactics
Journal of Automated Reasoning | 2021-06-09 | Paper |
Machine learning guidance for connection tableaux
Journal of Automated Reasoning | 2021-06-09 | Paper |
A survey of languages for formalizing mathematics
(available as arXiv preprint) | 2021-01-20 | Paper |
Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
Mathematics in Computer Science | 2020-10-30 | Paper |
Relaxed weighted path order in theorem proving
Mathematics in Computer Science | 2020-10-30 | Paper |
| Certification of nonclausal connection tableaux proofs | 2020-05-14 | Paper |
GRUNGE: a grand unified ATP challenge
(available as arXiv preprint) | 2020-03-10 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
Semantics of Mizar as an Isabelle object logic
Journal of Automated Reasoning | 2019-09-02 | Paper |
Isabelle formalization of set theoretic structures and set comprehensions
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
TacticToe: learning to reason with HOL4 tactics
EPiC Series in Computing | 2019-01-10 | Paper |
Deep network guided proof search
EPiC Series in Computing | 2019-01-10 | Paper |
Concrete semantics with Coq and CoqHammer
(available as arXiv preprint) | 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
(available as arXiv preprint) | 2018-10-18 | Paper |
| Towards formal foundations for game theory | 2018-10-04 | Paper |
Hammer for Coq: automation for dependent type theory
Journal of Automated Reasoning | 2018-08-21 | Paper |
| Towards a unified ordering for superposition-based automated reasoning | 2018-08-17 | Paper |
Aligning concepts across proof assistant libraries
Journal of Symbolic Computation | 2018-06-14 | Paper |
| Automating formalization by statistical and semantic parsing of mathematics | 2018-01-04 | Paper |
Monte Carlo tableau proof search
(available as arXiv preprint) | 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
Frontiers of Combining Systems | 2017-02-27 | Paper |
Random forests for premise selection
Frontiers of Combining Systems | 2017-02-27 | Paper |
A learning-based fact selector for Isabelle/HOL
Journal of Automated Reasoning | 2016-10-27 | Paper |
What's in a theorem name?
Interactive Theorem Proving | 2016-10-27 | Paper |
MizAR 40 for Mizar 40
Journal of Automated Reasoning | 2016-05-26 | Paper |
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Sharing HOL4 and HOL Light proof knowledge
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Efficient Low-Level Connection Tableaux
Lecture Notes in Computer Science | 2015-12-11 | Paper |
System description: E.T. 0.1
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Formalizing physics: automation, presentation and foundation issues
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Learning to parse on aligned corpora (rough diamond)
Interactive Theorem Proving | 2015-09-14 | Paper |
Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)''
Journal of Automated Reasoning | 2015-07-02 | Paper |
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Journal of Automated Reasoning | 2015-06-23 | Paper |
HOL(y)Hammer: online ATP service for HOL Light
Mathematics in Computer Science | 2015-03-25 | Paper |
Learning-assisted theorem proving with millions of lemmas
Journal of Symbolic Computation | 2015-01-14 | Paper |
Towards Knowledge Management for HOL Light
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Matching concepts across HOL libraries
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Developing corpus-based translation methods between informal and formal mathematics: project description
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Lemma Mining over HOL Light
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Web interfaces for proof assistants
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Algebraic analysis of Huzita's origami operations and their extensions
Automated Deduction in Geometry | 2013-09-20 | Paper |
Automated reasoning service for HOL Light
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Formal mathematics on display: a wiki for Flyspeck
Lecture Notes in Computer Science | 2013-08-09 | Paper |
Communicating formal proofs: the case of Flyspeck
Interactive Theorem Proving | 2013-08-07 | Paper |
MaSh: machine learning for Sledgehammer
Interactive Theorem Proving | 2013-08-07 | Paper |
Scalable LCF-style proof translation
Interactive Theorem Proving | 2013-08-07 | Paper |
PRocH: proof reconstruction for HOL Light
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Logical Methods in Computer Science | 2012-07-03 | Paper |
Reasoning about constants in Nominal Isabelle or how to formalize the second fixed point theorem
Certified Programs and Proofs | 2011-11-22 | Paper |
Proof assistant decision procedures for formalizing origami
Lecture Notes in Computer Science | 2011-07-29 | Paper |
General bindings and alpha-equivalence in Nominal Isabelle
Programming Languages and Systems | 2011-05-19 | Paper |
| Computing with classical real numbers | 2009-10-22 | Paper |
Merging Procedural and Declarative Proof
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Automating Side Conditions in Formalized Partial Functions
Lecture Notes in Computer Science | 2009-01-27 | Paper |
Certified Computer Algebra on Top of an Interactive Theorem Prover
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Cooperative Repositories for Formal Proofs
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
