| Publication | Date of Publication | Type |
|---|
| Invariant neural architecture for learning term synthesis in instantiation proving | 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 | 2023-11-16 | Paper |
| Hammering Mizar by Learning Clause Guidance (Short Paper). | 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) | 2022-11-09 | Paper |
| Prolog Technology Reinforcement Learning Prover | 2022-11-09 | Paper |
| Towards finding longer proofs | 2022-05-25 | Paper |
| The role of entropy in guiding a connection prover | 2022-05-25 | Paper |
| Learning theorem proving components | 2022-05-25 | Paper |
| Online machine learning techniques for Coq: a comparison | 2022-04-22 | Paper |
| Learning to solve geometric construction problems from images | 2022-04-22 | Paper |
| Fast and slow enigmas and parental guidance | 2022-03-24 | 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 |
| Hierarchical invention of theorem proving strategies | 2021-01-20 | Paper |
| The Tactician. A seamless, interactive tactic learner and prover for Coq | 2021-01-20 | Paper |
| First neural conjecturing datasets and experiments | 2021-01-20 | Paper |
| Guiding inferences in connection tableau by recurrent neural networks | 2021-01-20 | Paper |
| ENIGMAWatch: ProofWatch meets ENIGMA | 2020-05-14 | Paper |
| ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) | 2020-03-10 | Paper |
| GRUNGE: a grand unified ATP challenge | 2020-03-10 | Paper |
| Hammering towards QED | 2019-09-18 | Paper |
| TacticToe: learning to reason with HOL4 tactics | 2019-01-10 | Paper |
| Enhancing ENIGMA given clause guidance | 2018-10-18 | Paper |
| ATPboost: learning premise selection in binary setting with ATP feedback | 2018-10-18 | Paper |
| System description: XSL-based translator of Mizar to {\LaTeX} | 2018-10-18 | Paper |
| First experiments with neural translation of informal to formal mathematics | 2018-10-18 | Paper |
| ProofWatch: watchlist guidance for large theories in E | 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 | 2017-11-10 | Paper |
| Monte Carlo tableau proof search | 2017-09-22 | Paper |
| Detecting inconsistencies in large first-order knowledge bases | 2017-09-22 | Paper |
| ENIGMA: efficient learning-based inference guiding machine | 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 | 2017-02-27 | Paper |
| A learning-based fact selector for Isabelle/HOL | 2016-10-27 | Paper |
| Extending E prover with similarity based clause selection strategies | 2016-08-30 | Paper |
| Extracting Higher-Order Goals from the Mizar Mathematical Library | 2016-08-30 | Paper |
| MizAR 40 for Mizar 40 | 2016-05-26 | Paper |
| MaLeS: a framework for automatic tuning of automated theorem provers | 2016-05-26 | Paper |
| FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover | 2016-01-12 | Paper |
| System description: E.T. 0.1 | 2015-12-02 | Paper |
| Mizar: state-of-the-art and beyond | 2015-11-20 | Paper |
| Formalizing physics: automation, presentation and foundation issues | 2015-11-20 | Paper |
| Learning to parse on aligned corpora (rough diamond) | 2015-09-14 | Paper |
| Premise selection for mathematics by corpus analysis and kernel methods | 2015-07-02 | 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 |
| 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 |
| Presenting and explaining Mizar | 2013-12-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 |
| PRocH: proof reconstruction for HOL Light | 2013-06-14 | Paper |
| E-MaLeS 1.1 | 2013-06-14 | Paper |
| MPTP 0.1 -- system description | 2013-04-19 | Paper |
| The Mizar Mathematical Library in OMDoc: translation and applications | 2013-04-17 | Paper |
| ATP and presentation service for Mizar formalizations | 2013-04-17 | Paper |
| Theorem proving in large formal mathematics as an emerging AI field | 2013-04-16 | Paper |
| Dependencies in formal mathematics: applications and extraction for Coq and Mizar | 2012-09-07 | Paper |
| Point-and-write -- documenting formal mathematics by reference | 2012-09-07 | Paper |
| Overview and evaluation of premise selection techniques for large theory mathematics | 2012-09-05 | Paper |
| Automated and human proofs in general mathematics: an initial comparison | 2012-06-15 | Paper |
| Licensing the Mizar Mathematical Library (MML) | 2011-07-29 | Paper |
| Large formal wikis: issues and solutions | 2011-07-29 | Paper |
| Learning2Reason | 2011-07-29 | Paper |
| Automated proof compression by invention of new definitions | 2011-01-07 | Paper |
| Evaluation of automated theorem proving on the Mizar mathematical library | 2010-09-14 | Paper |
| Automated reasoning and presentation support for formalizing mathematics in MizAR | 2010-08-24 | Paper |
| A Wiki for Mizar: motivation, considerations, and initial prototype | 2010-08-24 | Paper |
| ATP-based cross-verification of Mizar proofs: method, systems, and first experiments | 2009-09-18 | Paper |
| MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance | 2008-11-27 | Paper |
| ATP Cross-Verification of the Mizar MPTP Challenge Problems | 2008-05-15 | Paper |
| MPTP 0.2: Design, implementation, and initial experiments | 2007-05-03 | Paper |
| MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics | 2007-02-20 | Paper |
| Mathematical Knowledge Management | 2007-02-12 | Paper |
| Mathematical Knowledge Management | 2005-08-26 | Paper |
| MPTP-motivation, implementation, first experiments | 2005-06-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4413895 | 2003-07-21 | Paper |
