| 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 |
| 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 |
| 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 |
| https://portal.mardi4nfdi.de/entity/Q2988060 | 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 | 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 |
