25 citations · 40 across the 2 of their papers we have counts for
3 papers
cs.CL2022★ 25 cited
HyperTree Proof Search for Neural Theorem Proving
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril +5
We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by…
cs.PL2020★ 15 cited
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…
cs.LO2018
Fast Cut-Elimination using Proof Terms: An Empirical Study
Gabriel Ebner
Urban and Bierman introduced a calculus of proof terms for the sequent calculus LK with a strongly normalizing reduction relation. We extend this calculus to simply-typed higher-or…