
Learned Provability Likelihood for Tactical Search
We present a method to estimate the provability of a mathematical formul...
read it

Tree Neural Networks in HOL4
We present an implementation of tree neural networks within the proof as...
read it

SelfLearned Formula Synthesis in Set Theory
A reinforcement learning algorithm accomplishes the task of synthesizing...
read it

Deep Reinforcement Learning in HOL4
The paper describes an implementation of deep reinforcement learning thr...
read it

GRUNGE: A Grand Unified ATP Challenge
This paper describes a large set of related theorem proving problems obt...
read it

Learning to Prove with Tactics
We implement a automated tactical prover TacticToe on top of the HOL4 in...
read it

Learning to Reason with HOL4 tactics
Techniques combining machine learning with translation to automated reas...
read it

Premise Selection and External Provers for HOL4
Learningassisted automated reasoning has recently gained popularity amo...
read it

Sharing HOL4 and HOL Light proof knowledge
New proof assistant developments often involve concepts similar to alrea...
read it
Thibault Gauthier
is this you? claim profile