Fetching the paper…
Reading the bibliography…
Large computer-understandable proofs consist of millions of intermediate logical steps.
A formulation of the simple theory of types
Alonzo Church · 1940
Earlier work this paper cites.
The principal type-scheme of an object in combinatory logic
R. Hindley · 1969
Earlier work this paper cites.
Hammering towards QED
Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban · 1972
Earlier work this paper cites.
Edinburgh LCF , volume 78 of Lecture Notes in Computer Science
Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth · 1979
Earlier work this paper cites.
Mizar in a nutshell
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz · 1980
Earlier work this paper cites.
Long short-term memory
Sepp Hochreiter and Jürgen Schmidhuber · 1997
Earlier work this paper cites.
Term rewriting and all that
Franz Baader and Tobias Nipkow · 1998
Earlier work this paper cites.
A generic tableau prover and its integration with Isabelle
Lawrence C. Paulson · 1999
Earlier work this paper cites.
First-order proof tactics in higher-order logic theorem provers
Joe Hurd · 2003
Earlier work this paper cites.
Importing HOL into Isabelle/HOL
Steven Obua and Sebastian Skalberg · 2006
Earlier work this paper cites.
The Use of Data-Mining for the Automatic Formation of Tactics
Hazel Duncan · 2007
Earlier work this paper cites.
ImageNet: A Large-Scale Hierarchical Image Database
J. Deng, W. Dong, R. Socher, L.-J. Li, K. Li, and L. Fei-Fei · 2009
Earlier work this paper cites.
HOL Light: An overview
John Harrison · 2009
Earlier work this paper cites.
Formal verification of a realistic compiler
Xavier Leroy · 2009
Earlier work this paper cites.
A revision of the proof of the Kepler Conjecture
Thomas Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller · 2010
Earlier work this paper cites.
Sine qua non for large theory reasoning
Kryštof Hoder and Andrei Voronkov · 2011
Cited alongside, same era.
The OpenTheory standard theory library
Joe Hurd · 2011
Cited alongside, same era.
MaLeCoP: Machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Cited alongside, same era.
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, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry · 2013
Cited alongside, same era.
The HOL Light theory of Euclidean space
John Harrison · 2013
Cited alongside, same era.
Scalable LCF-style proof translation
Cezary Kaliszyk and Alexander Krauss · 2013
Cited alongside, same era.
Comprehensive formal verification of an OS microkernel
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser · 2014
Later among the works it cites.
TensorFlow: Large-scale machine learning on heterogeneous systems, 2015
Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenberg, Dan Mané, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Kunal Talwar, Paul Tucker, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viégas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng · 2015
Later among the works it cites.
Mining the Archive of Formal Proofs
Jasmin Christian Blanchette, Maximilian P. L. Haslbeck, Daniel Matichuk, and Tobias Nipkow · 2015
Later among the works it cites.
A formal proof of the Kepler conjecture
Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller · 2015
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
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.
Reasoning with neural tensor networks for knowledge base completion
Richard Socher, Danqi Chen, Christopher D. Manning, and Andrew Y. Ng · 2013
Cited alongside, same era.
Recursive deep models for semantic compositionality over a sentiment treebank
Richard Socher, Alex Perelygin, Jean Wu, Jason Chuang, Christopher D. Manning, Andrew Y. Ng, and Christopher Potts · 2013
Cited alongside, same era.
Premise selection for mathematics by corpus analysis and kernel methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014
Cited alongside, same era.
Machine learning for first-order theorem proving - learning to select a good heuristic
James P. Bridge, Sean B. Holden, and Lawrence C. Paulson · 2014
Cited alongside, same era.
Later among the works it cites.
FEMaLeCoP: Fairly efficient machine learning connection prover
Cezary Kaliszyk and Josef Urban · 2015
Later among the works it cites.
Learning to parse on aligned corpora
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil · 2015
Later among the works it cites.
MaLeS: A framework for automatic tuning of automated theorem provers
Daniel Kühlwein and Josef Urban · 2015
Later among the works it cites.
End-to-end memory networks
Sainbayar Sukhbaatar, Jason Weston, Rob Fergus, et al · 2015
Later among the works it cites.
DeepMath – Deep sequence models for premise selection
Alex A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban · 2016
Later among the works it cites.
What’s in a theorem name?
David Aspinall and Cezary Kaliszyk · 2016
Later among the works it cites.
Using crash Hoare logic for certifying the FSCQ file system
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich · 2016
Later among the works it cites.
Internal guidance for Satallax
Michael Färber and Chad E. Brown · 2016
Later among the works it cites.
Mastering the game of go with deep neural networks and tree search
David Silver, Aja Huang, Christopher J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy Lillicrap, Madeleine Leach, Koray Kavukcuoglu, Thore Graepel, and Demis Hassabis · 2016
Later among the works it cites.
The CADE ATP system competition - CASC
Geoff Sutcliffe · 2016
Later among the works it cites.
Google’s neural machine translation system: Bridging the gap between human and machine translation
Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, Nishant Patil, Wei Wang, Cliff Young, Jason Smith, Jason Riesa, Alex Rudnick, Oriol Vinyals, Greg Corrado, Macduff Hughes, and Jeffrey Dean · 2016
Later among the works it cites.