most citedTacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

6 citations · 6 across the 3 of their papers we have counts for

collaborators
Showing cs.LOShow all

1 paper · 1 filter

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…