LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions

The macsyma system

William A Martin and Richard J Fateman · 1971

Earlier work this paper cites.

Isabelle/HOL: a proof assistant for higher-order logic

Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson · 2002

Earlier work this paper cites.

The lean theorem prover (system description)

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015

Earlier work this paper cites.

Propositions as types

Philip Wadler · 2015

Earlier work this paper cites.

Thinking fast and slow with deep learning and tree search

Thomas Anthony, Zheng Tian, and David Barber · 2017

Earlier work this paper cites.

Deepcoder: Learning to write programs

M Balog, AL Gaunt, M Brockschmidt, S Nowozin, and D Tarlow · 2017

Earlier work this paper cites.

Reinforcement learning of theorem proving

Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018

Cited alongside, same era.

A general reinforcement learning algorithm that masters chess, shogi, and go through self-play

David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al · 2018

Cited alongside, same era.

Holist: An environment for machine learning of higher order logic theorem proving

Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox · 2019

Cited alongside, same era.

Assessing mathematics misunderstandings via bayesian inverse planning

Anna N Rafferty, Rachel A Jansen, and Thomas L Griffiths · 2020

Cited alongside, same era.

Dreamcoder: Bootstrapping inductive program synthesis with wake-sleep library learning

Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, and Joshua B Tenenbaum · 2021

Cited alongside, same era.

Contrastive reinforcement learning of symbolic reasoning domains

Gabriel Poesia, WenXin Dong, and Noah Goodman · 2021

Later among the works it cites.

Leveraging language to learn program abstractions and search heuristics

Catherine Wong, Kevin M Ellis, Joshua Tenenbaum, and Jacob Andreas · 2021

Later among the works it cites.

Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning

Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli · 2021

Later among the works it cites.

Hypertree proof search for neural theorem proving

Original

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix · 2022

Closest in time.

Formal mathematics statement curriculum learning

Original

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022