Fetching the paper…
Reading the bibliography…
In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance.
Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban · 1972
Earlier work this paper cites.
Translating mizar for first order theorem provers
Josef Urban · 2003
Earlier work this paper cites.
Efficient and high quality force-directed graph drawing
Y. F. Hu · 2005
Earlier work this paper cites.
The four colour theorem: Engineering of a formal proof
Georges Gonthier · 2008
Earlier work this paper cites.
A modular integration of SAT/SMT solvers to coq through proof witnesses
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner · 2011
Earlier work this paper cites.
Machine learning in proof general
Ekaterina Komendantskaya, Jonathan Heras, and Gudmund Grov · 2013
Earlier work this paper cites.
Mash: Machine learning for sledgehammer
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban · 2013
Earlier work this paper cites.
Machine learning of coq proof guidance: First experiments
Cezary Kaliszyk, Lionel Mamane, and Josef Urban · 2014
Earlier work this paper cites.
TensorFlow: Large-scale machine learning on heterogeneous systems
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, Dandelion 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
Earlier work this paper cites.
Sepia: Search for proofs using inferred automata
Thomas Gransden, Neil Walkinshaw, and Rajeev Raman · 2015
Earlier work this paper cites.
Mizar 40 for mizar 40
Cezary Kaliszyk and Josef Urban · 2015
Earlier work this paper cites.
Tactictoe: Learning to reason with hol4 tactics
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban · 2017
Earlier work this paper cites.
ENIGMA: efficient learning-based inference guiding machine
Jan Jakubuv and Josef Urban · 2017
Earlier work this paper cites.
Hammer for coq: Automation for dependent type theory
Lukasz Czajka and Cezary Kaliszyk · 2018
Earlier work this paper 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
Earlier work this paper cites.
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E
Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban · 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.
Language models are unsupervised multitask learners
Alec Radford, Jeff Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever · 2019
Cited alongside, same era.
Learning to prove theorems via interacting with proof assistants
Kaiyu Yang and Jia Deng · 2019
Cited alongside, same era.
Tactic learning and proving for the coq proof assistant
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers · 2020
Cited alongside, same era.
The tactician - A seamless, interactive tactic learner and prover for coq
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers · 2020
Online machine learning techniques for coq: A comparison
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Černỳ, Cezary Kaliszyk, and Josef Urban · 2021
Later among the works it cites.
TF-GNN: graph neural networks in tensorflow
Oleksandr Ferludin, Arno Eigenwillig, Martin Blais, Dustin Zelle, Jan Pfeifer, Alvaro Sanchez-Gonzalez, Sibon Li, Sami Abu-El-Haija, Peter Battaglia, Neslihan Bulut, Jonathan Halcrow, Filipe Miguel Gonçalves de Almeida, Silvio Lattanzi, André Linhares, Brandon Mayer, Vahab Mirrokni, John Palowitch, Mihir Paradkar, Jennifer She, Anton Tsitsulin, Kevin Villela, Lisa Wang, David Wong, and Bryan Perozzi · 2022
Later among the works it cites.
Diversity-driven automated formal verification
Emily First and Yuriy Brun · 2022
Later among the works it cites.
The isabelle ENIGMA
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, and Josef Urban · 2022
Later among the works it cites.
Thor: Wielding hammers to integrate language models and automated theorem provers
Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik · 2022
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Practical proof search for coq by type inhabitation
Lukasz Czajka · 2020
Cited alongside, same era.
Tactok: Semantics-aware proof synthesis
Emily First, Yuriy Brun, and Arjun Guha · 2020
Cited alongside, same era.
ENIGMA anonymous: Symbol-independent inference guiding machine (system description)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban · 2020
Cited alongside, same era.
Graph representations for higher-order logic and theorem proving
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy · 2020
Cited alongside, same era.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Cited alongside, same era.
Generating correctness proofs with neural networks
Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner · 2020
Cited alongside, same era.
Later among the works it cites.
Hypertree proof search for neural theorem proving
Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet · 2022
Later among the works it cites.
Tactician’s web of large-scale formal knowledge, December 2023
Lasse Blaauwbroek · 2023
Later among the works it cites.
Magnushammer: A transformer-based approach to premise selection
Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2023
Later among the works it cites.
Machine-learned premise selection for lean
Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers · 2023
Later among the works it cites.
Artifact for: Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem Proving, December 2023
Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun · 2023
Later among the works it cites.
Passport: Improving automated formal verification using identifiers
Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer · 2023
Later among the works it cites.
The Coq Proof Assistant, July 2023
The Coq Development Team · 2023
Later among the works it cites.
LeanDojo: Theorem proving with retrieval-augmented language models
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar · 2023
Later among the works it cites.
The Tactician’s web of large-scale formal knowledge
Lasse Blaauwbroek · 2024
Closest in time.
Hashing modulo context-sensitive α \alpha -equivalence
Lasse Blaauwbroek, Miroslav Olšák, and Herman Geuvers · 2024
Closest in time.