EUROPROOFNET-WG5: THEOREM PROVING AND MACHINE LEARNING IN THE AGE OF LLMS

This page contains an index consisting of author-provided keywords.

A
Abductive Reasoning	Proof By Abduction in Isabelle/HOL
Abstract syntax tree	Kernel-level expression generator
Abstraction	Abstraction Logic Is All You Need
agda	Structure-Aware Neural Representations of Agda Programs Correct by Construction Machine Learning
AI in mathematics	Mathematics and Creative AI
Algebra	Abstraction Logic Is All You Need
Andrews-Curtis conjecture	In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics
Artificial intelligence	Automated Theorem Provers as the Hub of the AI Math Ecosystem
autoformalization	Autoformalization and autoinformalization via probabilistic reasoning
autoinformalization	Autoformalization and autoinformalization via probabilistic reasoning
Automated reasoning	Automated Theorem Provers as the Hub of the AI Math Ecosystem
automated theorem proving	The need for ethical guidelines in mathematical research in the time of generative AI In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics Intrinsic Motivation To Construct Terms In A Dependent Type Theory On Abstract Logics for Interacting Provers
automatisation of mathematics	Mathematics and Creative AI
B
benchmark	CoqPilot benchmarking framework
C
cnn	Correct by Construction Machine Learning
code generation	CoqPilot benchmarking framework
Conjecturing	Proof By Abduction in Isabelle/HOL
Conjunctive Normal Form	Reinforcement Learning for Term Rewrite Systems
consistency	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
controlled generation	Autoformalization and autoinformalization via probabilistic reasoning
Coq	CoqPilot benchmarking framework How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
creativity	Chessboard covers and AI.
crystallography	From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
cylindrical decomposition	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
D
data processing for large scale APT	In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics
dataset	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study
Deductive Program Verification	Towards LLM-support for Deductive Verification of Java Programs
Dependent Type Theory	Intrinsic Motivation To Construct Terms In A Dependent Type Theory
dependent types	Structure-Aware Neural Representations of Agda Programs Correct by Construction Machine Learning
Dialogue	The Fatio Protocol for Formal Dialogue in Isabelle/HOL
dimers and monomers	Chessboard covers and AI.
E
Explainable AI	Transformers to Predict the Applicability of Symbolic Integration Routines
F
fine-tuning and alignment	Between min cost search and least action
Formal Mathematics	Automated Theorem Provers as the Hub of the AI Math Ecosystem Intrinsic Motivation To Construct Terms In A Dependent Type Theory
formal proofs	Chessboard covers and AI.
Formal Verification	Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover
G
Generative AI	Are LLMs Ready for Software Verification?
GPT	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
I
Institutions	On Abstract Logics for Interacting Provers
interactive theorem proving	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Isabelle	DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
Isabelle/HOL	Proof By Abduction in Isabelle/HOL
J
Java Modelling Language	Towards LLM-support for Deductive Verification of Java Programs
L
large language model	Are LLMs Ready for Software Verification? MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant
Large Language Models	Neuro-Symbolic Lemma Conjecturing NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving Towards LLM-support for Deductive Verification of Java Programs Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover Autoformalization and autoinformalization via probabilistic reasoning On Abstract Logics for Interacting Provers
Lean	Kernel-level expression generator Chessboard covers and AI.
least action principle	Between min cost search and least action
Lemma conjecturing	Neuro-Symbolic Lemma Conjecturing
LLM	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving CoqPilot benchmarking framework Chessboard covers and AI. How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
LLM agents	NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Logic	Abstraction Logic Is All You Need
Logical Frameworks	Abstraction Logic Is All You Need
M
machine learning	In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics Transformers to Predict the Applicability of Symbolic Integration Routines DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant On Abstract Logics for Interacting Provers From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
Mathematical creativity	Mathematics and Creative AI
Mathematical Foundations	Abstraction Logic Is All You Need
mathematical practice	The need for ethical guidelines in mathematical research in the time of generative AI
min cost search	Between min cost search and least action
Mona and finite-state methods	Between min cost search and least action
Multi-Agent systems	The Fatio Protocol for Formal Dialogue in Isabelle/HOL
N
Natural Deduction	Abstraction Logic Is All You Need
Natural Language Processing	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
Neural Theorem Proving	Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover
O
Ontology	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
orphic diagrams	From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
P
premise selection	Structure-Aware Neural Representations of Agda Programs
probabilistic programming	Autoformalization and autoinformalization via probabilistic reasoning
probability	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
proof assistant	Kernel-level expression generator DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
Proof assistants	The Fatio Protocol for Formal Dialogue in Isabelle/HOL
Proof automation	NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Proof Tactics	Proof By Abduction in Isabelle/HOL
proof translation	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study
Proximal Policy Optimization	Reinforcement Learning for Term Rewrite Systems
Python	Reinforcement Learning for Term Rewrite Systems
R
random forest	From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
Recurrent neural network	Kernel-level expression generator
Reinforcement Learning	Intrinsic Motivation To Construct Terms In A Dependent Type Theory Reinforcement Learning for Term Rewrite Systems Kernel-level expression generator DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant
representation learning	Structure-Aware Neural Representations of Agda Programs
research ethics	The need for ethical guidelines in mathematical research in the time of generative AI
S
Satisfiability	Reinforcement Learning for Term Rewrite Systems
semi-algebraic sets	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
Sequent Calculus	Abstraction Logic Is All You Need
sequential Monte Carlo	Autoformalization and autoinformalization via probabilistic reasoning
Software verification	Are LLMs Ready for Software Verification?
Specification Generation	Towards LLM-support for Deductive Verification of Java Programs
Symbolic Integration	Transformers to Predict the Applicability of Symbolic Integration Routines
symmetries	From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
T
Tarski Seidenberg	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
Term Rewrite System	Reinforcement Learning for Term Rewrite Systems
theorem provers	Correct by Construction Machine Learning
theorem proving	Reinforcement Learning for Term Rewrite Systems DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant
Theory exploration	Neuro-Symbolic Lemma Conjecturing
Transformers	Transformers to Predict the Applicability of Symbolic Integration Routines Chessboard covers and AI.
Type checker	Kernel-level expression generator
V
VC dimension	Chessboard covers and AI.

Disclaimer | Powered by EasyChair Smart Program