Fetching the paper…
Reading the bibliography…
In theorem proving, the task of selecting useful premises from a large library to unlock the proof of a given conjecture is crucially important.
Realization of a geometry theorem proving machine
Herbert L Gelernter · 1959
Earlier work this paper cites.
A machine program for theorem-proving
Martin Davis, George Logemann, and Donald Loveland · 1962
Earlier work this paper cites.
Truth and proof
Alfred Tarski · 1969
Earlier work this paper cites.
The complexity of theorem-proving procedures
Stephen A Cook · 1971
Earlier work this paper cites.
Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban · 1972
Earlier work this paper cites.
A formally verified proof of the prime number theorem
Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff · 2007
Earlier work this paper cites.
SRASS - A semantic relevance axiom selection system
Geoff Sutcliffe and Yury Puzis · 2007
Earlier work this paper cites.
Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007 , volume 257 of CEUR Workshop Proceedings , 2007. CEUR-WS.org
Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors · 2007
Earlier work this paper cites.
Malarea: a metasystem for automated reasoning in large theories
Josef Urban · 2007
Earlier work this paper cites.
Formal proof–the four-color theorem
Georges Gonthier et al · 2008
Earlier work this paper cites.
Translating higher-order clauses to first-order clauses
Jia Meng and Lawrence C. Paulson · 2008
Earlier work this paper cites.
Malarea SG1- machine learner for automated reasoning with semantic guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil · 2008
Earlier work this paper cites.
sel4: Formal verification of an os kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al · 2009
Earlier work this paper cites.
Propagation via lazy clause generation
Olga Ohrimenko, Peter J Stuckey, and Michael Codish · 2009
Cited alongside, same era.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2009
Cited alongside, same era.
Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers
Lawrence C. Paulson · 2010
Cited alongside, same era.
Sine qua non for large theory reasoning
Kryštof Hoder and Andrei Voronkov · 2011
Cited alongside, same era.
Overview and evaluation of premise selection techniques for large theory mathematics
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes · 2012
Cited alongside, same era.
A machine-checked proof of the odd order theorem
Hammer for coq: Automation for dependent type theory
Lukasz Czajka and Cezary Kaliszyk · 2018
Later among the works it cites.
Language models are unsupervised multitask learners
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al · 2019
Later among the works it cites.
Serapis: A concept-oriented search engine for the isabelle libraries based on natural language
Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, and LC Paulson · 2020
Later among the works it cites.
The pile: An 800gb dataset of diverse text for language modeling, 2021
Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy · 2021
Later among the works it cites.
Proof artifact co-training for theorem proving with language models
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu · 2021
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al · 2013
Cited alongside, same era.
Premise selection and external provers for HOL4
Thibault Gauthier and Cezary Kaliszyk · 2015
Cited alongside, same era.
Hol(y)hammer: Online ATP service for HOL light
Cezary Kaliszyk and Josef Urban · 2015
Cited alongside, same era.
Deepmath-deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban · 2016
Cited alongside, same era.
Holstep: A machine learning dataset for higher-order logic theorem proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Cited alongside, same era.
Mastering chess and shogi by self-play with a general reinforcement learning algorithm
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis · 2017
Cited alongside, same era.
Attention is all you need, 2017
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin · 2017
Cited alongside, same era.
Later among the works it cites.
Lisa: Language models of isabelle proofs
Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Later among the works it cites.
Isarstep: a benchmark for high-level mathematical reasoning
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson · 2021
Later among the works it cites.
Liquid tensor experiment
Peter Scholze · 2021
Later among the works it cites.
Roformer: Enhanced transformer with rotary position embedding, 2021
Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu · 2021
Later among the works it cites.
GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model
Ben Wang and Aran Komatsuzaki · 2021
Later among the works it cites.
Formal mathematics statement curriculum learning
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Closest in time.
minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2022
Closest in time.