Learning conjecturing from scratch

DOI10.1007/978-3-031-99984-0_23MaRDI QIDQ6869937zbMATH OpenFDO

Authors T. Gauthier, Josef Urban

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_23

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A mathematical benchmark for inductive theorem provers
• A procedure for proving special function inequalities involving a discrete parameter
• A Short Presentation of Coq
• Alien coding
• ATPboost: learning premise selection in binary setting with ATP feedback
• Dynamic rippling, middle-out reasoning and lemma discovery
• First experiments with neural translation of informal to formal mathematics
• First neural conjecturing datasets and experiments
• Guessing with little data
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Handbook of automated reasoning. In 2 vols
• scientific article; zbMATH DE number 872231 (Why is no real title available?)
• Induction for SMT solvers
• Integer induction in saturation
• Invariant neural architecture for learning term synthesis in instantiation proving
• Learning guided automated reasoning: a brief survey
• Lemma discovery and strategies for automated induction
• Machine Learning for Inductive Theorem Proving
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• Rippling: A heuristic for guiding inductive proofs
• Stateful premise selection by recurrent neural networks
• Targeted configuration of an SMT solver
• Tests and proofs. 4th international conference, TAP 2010, Málaga, Spain, July 1--2, 2010. Proceedings
• The Isabelle Framework
• The On-Line Encyclopedia of Integer Sequences
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Vampire with a brain is a good ITP hammer

This page was built for publication: Learning conjecturing from scratch

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869937)