Fetching the paper…
Reading the bibliography…
Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built.
Holist: An environment for machine learning of higher-order theorem proving (extended version)
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox · 1904
Earlier work this paper cites.
Learning to reason in large theories without imitation
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy · 1905
Earlier work this paper cites.
Inductively defined types in the calculus of constructions
Frank Pfenning and Christine Paulin-Mohring · 1989
Earlier work this paper cites.
The De Bruijn factor, 2000
Freek Wiedijk · 2000
Earlier work this paper cites.
Scaling laws for neural language models
Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei · 2001
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2009
Earlier work this paper cites.
Scaling laws for autoregressive generative modeling
Tom Henighan, Jared Kaplan, Mor Katz, Mark Chen, Christopher Hesse, Jacob Jackson, Heewoo Jun, Tom B. Brown, Prafulla Dhariwal, Scott Gray, Chris Hallacy, Benjamin Mann, Alec Radford, Aditya Ramesh, Nick Ryder, Daniel M. Ziegler, John Schulman, Dario Amodei, and Sam McCandlish · 2010
Earlier work this paper cites.
Learning-assisted theorem proving with millions of lemmas
Cezary Kaliszyk and Josef Urban · 2014
Earlier work this paper cites.
The lean theorem prover (system description)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015
Earlier work this paper cites.
Sharing HOL4 and HOL light proof knowledge
Thibault Gauthier and Cezary Kaliszyk · 2015
Earlier work this paper cites.
Lemmatization for stronger reasoning in large theories
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil · 2015
Earlier work this paper cites.
Holophrasm: a neural automated theorem prover for higher-order logic
Daniel Whalen · 2016
Earlier work this paper cites.
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura · 2017
Earlier work this paper cites.
A fully automatic theorem prover with human-style output
M. Ganesalingam and W. T. Gowers · 2017
Earlier work this paper cites.
Holstep: A machine learning dataset for higher-order logic theorem proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Cited alongside, same era.
First experiments with neural translation of informal to formal mathematics
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban · 2018
Cited alongside, same era.
Holist: An environment for machine learning of higher order logic theorem proving
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox · 2019
Cited alongside, same era.
Gamepad: A learning environment for theorem proving
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever · 2019
Cited alongside, same era.
fairseq: A fast, extensible toolkit for sequence modeling
Myle Ott, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng, David Grangier, and Michael Auli · 2019
Cited alongside, same era.
Learning to prove theorems via interacting with proof assistants
Generating correctness proofs with neural networks
Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner · 2020
Later among the works it cites.
Liquid tensor experiment
Peter Scholze · 2020
Later among the works it cites.
First neural conjecturing datasets and experiments
Josef Urban and Jan Jakubuv · 2020
Later among the works it cites.
Learning to prove theorems by learning to generate theorems
Mingzhe Wang and Jia Deng · 2020
Later among the works it cites.
Exploration of neural machine translation in autoformalization of mathematics in mizar
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban · 2020
Later among the works it cites.
Schemes in lean
Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison · 2021
Closest in time.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Kaiyu Yang and Jia Deng · 2019
Cited alongside, same era.
The tactician - A seamless, interactive tactic learner and prover for coq
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers · 2020
Cited alongside, same era.
Language models are few-shot learners
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei · 2020
Cited alongside, same era.
Formalising perfectoid spaces
Kevin Buzzard, Johan Commelin, and Patrick Massot · 2020
Cited alongside, same era.
A formal proof of the independence of the continuum hypothesis
Jesse Michael Han and Floris van Doorn · 2020
Cited alongside, same era.
Deep learning for symbolic mathematics
Guillaume Lample and François Charton · 2020
Cited alongside, same era.
The lean mathematical library
mathlib · 2020
Cited alongside, same era.
Learning advanced mathematical computations from examples
François Charton, Amaury Hayat, and Guillaume Lample · 2021
Closest in time.
An image is worth 16x16 words: Transformers for image recognition at scale
Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby · 2021
Closest in time.
Tactictoe: Learning to prove with tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish · 2021
Closest in time.
Teaching temporal logics to neural networks
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner · 2021
Closest in time.
Isarstep: a benchmark for high-level mathematical reasoning
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson · 2021
Closest in time.
Mathematical reasoning via self-supervised skip-tree training
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy · 2021
Closest in time.
Learning transferable visual models from natural language supervision
Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever · 2021
Closest in time.
LIME: learning inductive bias for primitives of mathematical reasoning
Yuhuai Wu, Markus N. Rabe, Wenda Li, Jimmy Ba, Roger B. Grosse, and Christian Szegedy · 2021
Closest in time.