Fetching the paper…
Reading the bibliography…
In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time.
Fast graph representation learning with pytorch geometric
Matthias Fey and Jan Eric Lenssen · 1903
Earlier work this paper cites.
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban · 1905
Earlier work this paper cites.
Deep graph library: Towards efficient and scalable deep learning on graphs
Minjie Wang, Lingfan Yu, Da Zheng, Quan Gan, Yu Gai, Zihao Ye, Mufei Li, Jinjing Zhou, Qi Huang, Chao Ma, Ziyue Huang, Qipeng Guo, Hao Zhang, Haibin Lin, Junbo Zhao, Jinyang Li, Alexander J. Smola, and Zheng Zhang · 1909
Earlier work this paper cites.
Deep reinforcement learning in HOL4
Thibault Gauthier · 1910
Earlier work this paper cites.
Am: An artificial intelligence approach to discovery in mathematics as heuristic search, sail aim-286
Douglas B Lenat · 1976
Earlier work this paper cites.
Natural deduction as higher-order resolution
Lawrence C. Paulson · 1986
Earlier work this paper cites.
On conjectures of graffiti
Siemion Fajtlowicz · 1988
Earlier work this paper cites.
An overview of the mizar project
Piotr Rudnicki · 1992
Earlier work this paper cites.
HOL Light: A tutorial introduction
John Harrison · 1996
Earlier work this paper cites.
Solution of the Robbins’ problem
William McCune · 1997
Earlier work this paper cites.
The Coq proof assistant reference manual
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al · 1999
Earlier work this paper cites.
Formal verification in hardware design: a survey
Christoph Kern and Mark R Greenstreet · 1999
Earlier work this paper cites.
Learning to prove theorems by learning to generate theorems
Mingzhe Wang and Jia Deng · 2002
Earlier work this paper cites.
Abstract algebra , volume 3
David Steven Dummit and Richard M Foote · 2004
Earlier work this paper cites.
A theorem proving approach to analysis of secure information flow
Ádám Darvas, Reiner Hähnle, and David Sands · 2005
Earlier work this paper cites.
Modelling high-level mathematical reasoning in mechanised declarative proofs
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson · 2006
Earlier work this paper cites.
Malarea: a metasystem for automated reasoning in large theories
Josef Urban · 2007
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.
Imagenet: A large-scale hierarchical image database
Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Fei-Fei Li · 2009
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2009
Earlier work this paper cites.
MaLeCoP machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Earlier work this paper cites.
Automated theory formation in pure mathematics
Simon Colton · 2012
Earlier work this paper cites.
A machine-checked proof of the odd order theorem
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
Earlier work this paper cites.
First-order theorem proving and Vampire
Laura Kovács and Andrei Voronkov · 2013
Cited alongside, same era.
System description: E 1.8
Stephan Schulz · 2013
Cited alongside, same era.
Machine learning for first-order theorem proving
James P. Bridge, Sean B. Holden, and Lawrence C. Paulson · 2014
Cited alongside, same era.
Hipster: Integrating theory exploration in a proof assistant
Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen · 2014
Cited alongside, same era.
Learning-assisted theorem proving with millions of lemmas
Cezary Kaliszyk and Josef Urban · 2014
Cited alongside, same era.
The Lean theorem prover (system description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer · 2015
Cited alongside, same era.
Mastering the game of Go without human knowledge
David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al · 2017
Later among the works it cites.
Attention is all you need
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin · 2017
Later among the works it cites.
Premise selection for theorem proving by deep graph embedding
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng · 2017
Later among the works it cites.
Learning to prove with tactics
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Sharing HOL4 and HOL light proof knowledge
Thibault Gauthier and Cezary Kaliszyk · 2015
Cited alongside, same era.
Lemmatization for stronger reasoning in large theories
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil · 2015
Cited alongside, same era.
Adam: A method for stochastic optimization
Diederik P. Kingma and Jimmy Ba · 2015
Cited alongside, same era.
Improved semantic representations from tree-structured long short-term memory networks
Kai Sheng Tai, Richard Socher, and Christopher D. Manning · 2015
Cited alongside, same era.
Initial experiments with statistical conjecturing over large formal corpora
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2016
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.
Bartosz Piotrowski and Josef Urban · 2018
Later among the works it cites.
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, Timothy Lillicrap, Karen Simonyan, and Demis Hassabis · 2018
Later among the works it cites.
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
Later among the works it cites.
First experiments with data driven conjecturing
Karel Chvalovskỳ, Thibault Gauthier, and Josef Urban · 2019
Later among the works it cites.
GamePad: A learning environment for theorem proving
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever · 2019
Later among the works it cites.
Hammering mizar by learning clause guidance (short paper)
Jan Jakubuv and Josef Urban · 2019
Later among the works it cites.
Metamath: A Computer Language for Mathematical Proofs
Norman Megill and David A Wheeler · 2019
Later among the works it cites.
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
Later among the works it cites.
Grandmaster level in StarCraft II using multi-agent reinforcement learning
Oriol Vinyals, Igor Babuschkin, Wojciech Marian Czarnecki, Michaël Mathieu, Andrew Joseph Dudzik, Junyoung Chung, Duck Hwan Choi, Richard W. Powell, Timo Ewalds, Petko Georgiev, Junhyuk Oh, Dan Horgan, Manuel Kroiss, Ivo Danihelka, Aja Huang, Laurent Sifre, Trevor Cai, John P. Agapiou, Max Jaderberg, Alexander Sasha Vezhnevets, Rémi Leblond, Tobias Pohlen, Valentin Dalibard, David Budden, Yury Sulsky, James Molloy, Tom Le Paine, Caglar Gulcehre, Ziyu Wang, Tobias Pfaff, Yuhuai Wu, Roman Ring, Dani Yogatama, Dario Wünsch, Katrina McKinney, Oliver Smith, Tom Schaul, Timothy P. Lillicrap, Koray Kavukcuoglu, Demis Hassabis, Chris Apps, and David Silver · 2019
Later among the works it cites.
How powerful are graph neural networks?
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka · 2019
Later among the works it cites.
Learning to prove theorems via interacting with proof assistants
Kaiyu Yang and Jia Deng · 2019
Later among the works it cites.
Deep reinforcement learning for synthesizing functions in higher-order logic
Thibault Gauthier · 2020
Closest in time.
ENIGMA anonymous: Symbol-independent inference guiding machine (system description)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban · 2020
Closest in time.
Mathematical reasoning in latent space
Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal · 2020
Closest in time.
Property invariant embedding for automated reasoning
Miroslav Olsák, Cezary Kaliszyk, and Josef Urban · 2020
Closest in time.
Mathematical reasoning via self-supervised skip-tree training
Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy · 2020
Closest in time.
First neural conjecturing datasets and experiments
Josef Urban and Jan Jakubv · 2020
Closest in time.