| Publication | Date of Publication | Type |
|---|
| Exploring formal math on the blockchain: an explorer for Proofgold | 2026-02-19 | Paper |
| Hammering higher order set theory | 2026-02-19 | Paper |
| Learning conjecturing from scratch | 2026-01-21 | Paper |
Machine learning for quantifier selection in cvc5
International Journal of Approximate Reasoning | 2026-01-21 | Paper |
| Stateful premise selection by recurrent neural networks | 2025-02-20 | Paper |
| A mathematical benchmark for inductive theorem provers | 2025-02-19 | Paper |
| Learning guided automated reasoning: a brief survey | 2025-02-07 | Paper |
Invariant neural architecture for learning term synthesis in instantiation proving
Journal of Symbolic Computation | 2024-12-09 | Paper |
| Solving hard Mizar problems with instantiation and strategy invention | 2024-12-04 | Paper |
| Automated theorem proving for Metamath | 2024-11-26 | 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 |
| Learning Proof Transformations and Its Applications in Interactive Theorem Proving | 2024-05-03 | Paper |
| Translating SUMO-K to Higher-Order Set Theory | 2024-05-03 | Paper |
Alien coding
International Journal of Approximate Reasoning | 2023-11-16 | Paper |
Hammering Mizar by Learning Clause Guidance (Short Paper).
(available as arXiv preprint) | 2023-02-03 | Paper |
| Guiding an automated theorem prover with neural rewriting | 2022-12-07 | Paper |
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Automated Reasoning | 2022-11-09 | Paper |
Prolog Technology Reinforcement Learning Prover
Automated Reasoning | 2022-11-09 | Paper |
Towards finding longer proofs
(available as arXiv preprint) | 2022-05-25 | Paper |
The role of entropy in guiding a connection prover
(available as arXiv preprint) | 2022-05-25 | Paper |
| The role of entropy in guiding a connection prover | 2022-05-25 | Paper |
Learning theorem proving components
(available as arXiv preprint) | 2022-05-25 | Paper |
Online machine learning techniques for Coq: a comparison
(available as arXiv preprint) | 2022-04-22 | Paper |
Learning to solve geometric construction problems from images
(available as arXiv preprint) | 2022-04-22 | Paper |
Fast and slow enigmas and parental guidance
(available as arXiv preprint) | 2022-03-24 | 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 |
The Tactician. A seamless, interactive tactic learner and prover for Coq
(available as arXiv preprint) | 2021-01-20 | Paper |
Guiding inferences in connection tableau by recurrent neural networks
(available as arXiv preprint) | 2021-01-20 | Paper |
First neural conjecturing datasets and experiments
(available as arXiv preprint) | 2021-01-20 | Paper |
Hierarchical invention of theorem proving strategies
AI Communications | 2021-01-20 | Paper |
ENIGMAWatch: ProofWatch meets ENIGMA
(available as arXiv preprint) | 2020-05-14 | Paper |
GRUNGE: a grand unified ATP challenge
(available as arXiv preprint) | 2020-03-10 | Paper |
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
(available as arXiv preprint) | 2020-03-10 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
TacticToe: learning to reason with HOL4 tactics
EPiC Series in Computing | 2019-01-10 | Paper |
| System description: XSL-based translator of Mizar to {\LaTeX} | 2018-10-18 | Paper |
| Enhancing ENIGMA given clause guidance | 2018-10-18 | Paper |
First experiments with neural translation of informal to formal mathematics
(available as arXiv preprint) | 2018-10-18 | Paper |
ATPboost: learning premise selection in binary setting with ATP feedback
(available as arXiv preprint) | 2018-10-18 | Paper |
ProofWatch: watchlist guidance for large theories in E
(available as arXiv preprint) | 2018-10-04 | Paper |
| Automating formalization by statistical and semantic parsing of mathematics | 2018-01-04 | Paper |
The CADE-25 automated theorem proving system competition -- CASC-25
AI Communications | 2017-11-10 | Paper |
| Detecting inconsistencies in large first-order knowledge bases | 2017-09-22 | Paper |
Monte Carlo tableau proof search
(available as arXiv preprint) | 2017-09-22 | Paper |
ENIGMA: efficient learning-based inference guiding machine
(available as arXiv preprint) | 2017-07-21 | Paper |
| A mathematical proof proved correct: the most efficient way to pack spheres | 2017-05-18 | Paper |
Lemmatization for stronger reasoning in large theories
Frontiers of Combining Systems | 2017-02-27 | Paper |
A learning-based fact selector for Isabelle/HOL
Journal of Automated Reasoning | 2016-10-27 | Paper |
Extracting Higher-Order Goals from the Mizar Mathematical Library
Lecture Notes in Computer Science | 2016-08-30 | Paper |
Extending E prover with similarity based clause selection strategies
Lecture Notes in Computer Science | 2016-08-30 | Paper |
MaLeS: a framework for automatic tuning of automated theorem provers
Journal of Automated Reasoning | 2016-05-26 | 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 |
System description: E.T. 0.1
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Mizar: state-of-the-art and beyond
Lecture Notes in Computer Science | 2015-11-20 | 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 |
Premise selection for mathematics by corpus analysis and kernel methods
Journal of Automated Reasoning | 2015-07-02 | 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 |
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 |
Presenting and explaining Mizar
Electronic Notes in Theoretical Computer Science | 2013-12-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 |
MaSh: machine learning for Sledgehammer
Interactive Theorem Proving | 2013-08-07 | Paper |
Communicating formal proofs: the case of Flyspeck
Interactive Theorem Proving | 2013-08-07 | Paper |
PRocH: proof reconstruction for HOL Light
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
E-MaLeS 1.1
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
MPTP 0.1 -- system description
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
ATP and presentation service for Mizar formalizations
Journal of Automated Reasoning | 2013-04-17 | Paper |
The Mizar Mathematical Library in OMDoc: translation and applications
Journal of Automated Reasoning | 2013-04-17 | Paper |
Theorem proving in large formal mathematics as an emerging AI field
Automated Reasoning and Mathematics | 2013-04-16 | Paper |
Dependencies in formal mathematics: applications and extraction for Coq and Mizar
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Point-and-write -- documenting formal mathematics by reference
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Overview and evaluation of premise selection techniques for large theory mathematics
Automated Reasoning | 2012-09-05 | Paper |
Automated and human proofs in general mathematics: an initial comparison
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
Large formal wikis: issues and solutions
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Licensing the Mizar Mathematical Library (MML)
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Learning2Reason
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Automated proof compression by invention of new definitions
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Evaluation of automated theorem proving on the Mizar mathematical library
Mathematical Software – ICMS 2010 | 2010-09-14 | Paper |
Automated reasoning and presentation support for formalizing mathematics in MizAR
Lecture Notes in Computer Science | 2010-08-24 | Paper |
A Wiki for Mizar: motivation, considerations, and initial prototype
Lecture Notes in Computer Science | 2010-08-24 | Paper |
ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
Mathematics in Computer Science | 2009-09-18 | Paper |
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
Automated Reasoning | 2008-11-27 | Paper |
ATP Cross-Verification of the Mizar MPTP Challenge Problems
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
MPTP 0.2: Design, implementation, and initial experiments
Journal of Automated Reasoning | 2007-05-03 | Paper |
MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
Journal of Applied Logic | 2007-02-20 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Mathematical Knowledge Management
Lecture Notes in Computer Science | 2005-08-26 | Paper |
MPTP-motivation, implementation, first experiments
Journal of Automated Reasoning | 2005-06-22 | Paper |
| scientific article; zbMATH DE number 1951640 (Why is no real title available?) | 2003-07-21 | Paper |
