2 papers
cs.LG2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Minchao Wu, Michael Norrish, Christian Walder +1
We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tacti…
cs.LO2021
A bi-directional extensible interface between Lean and Mathematica
Robert Y. Lewis, Minchao Wu
We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other…