Fetching the paper…
Reading the bibliography…
How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms - a game of conjecture and proof.
Introduction to metamathematics
Stephen Cole Kleene · 1952
Earlier work this paper cites.
The logic theory machine–a complex information processing system
Allen Newell and Herbert Simon · 1956
Earlier work this paper cites.
AM: an artificial intelligence approach to discovery in mathematics as heuristic search
Douglas Bruce Lenat · 1976
Earlier work this paper cites.
The calculus of constructions
Thierry Coquand and Gérard Huet · 1986
Earlier work this paper cites.
On the notion of interestingness in automated mathematical discovery
Simon Colton, Alan Bundy, and Toby Walsh · 2000
Earlier work this paper cites.
Minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2000
Earlier work this paper cites.
Intrinsically motivated reinforcement learning
Nuttapong Chentanez, Andrew Barto, and Satinder Singh · 2004
Earlier work this paper cites.
Bandit based monte-carlo planning
Levente Kocsis and Csaba Szepesvári · 2006
Earlier work this paper cites.
Intrinsic motivation systems for autonomous mental development
Pierre-Yves Oudeyer, Frdric Kaplan, and Verena V Hafner · 2007
Earlier work this paper cites.
Formal theory of creativity, fun, and intrinsic motivation (1990–2010)
Jürgen Schmidhuber · 2010
Earlier work this paper cites.
Powerplay: Training an increasingly general problem solver by continually searching for the simplest still unsolvable problem
Jürgen Schmidhuber · 2013
Earlier work this paper cites.
Unifying count-based exploration and intrinsic motivation
Marc Bellemare, Sriram Srinivasan, Georg Ostrovski, Tom Schaul, David Saxton, and Remi Munos · 2016
Earlier work this paper cites.
Deepmath-deep sequence models for premise selection
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban · 2016
Earlier work this paper cites.
Holophrasm: a neural automated theorem prover for higher-order logic
Daniel Whalen · 2016
Earlier work this paper cites.
Hindsight experience replay
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, OpenAI Pieter Abbeel, and Wojciech Zaremba · 2017
Earlier work this paper cites.
Curiosity-driven exploration by self-supervised prediction
Deepak Pathak, Pulkit Agrawal, Alexei A Efros, and Trevor Darrell · 2017
Earlier work this paper 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
Cited alongside, same era.
Exploration by random network distillation
Yuri Burda, Harrison Edwards, Amos Storkey, and Oleg Klimov · 2018
Cited alongside, same era.
Learning to play with intrinsically-motivated, self-aware agents
Nick Haber, Damian Mrowca, Stephanie Wang, Li F Fei-Fei, and Daniel L Yamins · 2018
Cited alongside, same era.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018
Cited alongside, same era.
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, et al · 2018
Cited alongside, same era.
Zero-shot text-to-image generation
Aditya Ramesh, Mikhail Pavlov, Gabriel Goh, Scott Gray, Chelsea Voss, Alec Radford, Mark Chen, and Ilya Sutskever · 2021
Later among the works it cites.
Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning
Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli · 2021
Later among the works it cites.
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample · 2022
Later among the works it cites.
Hypertree proof search for neural theorem proving
Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet · 2022
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
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Natural number game
Kevin Buzzard · 2019
Cited alongside, same era.
Learning with amigo: Adversarially motivated intrinsic goals
Andres Campero, Roberta Raileanu, Heinrich Küttler, Joshua B Tenenbaum, Tim Rocktäschel, and Edward Grefenstette · 2020
Cited alongside, same era.
Mathzero, the classification problem, and set-theoretic type theory
David McAllester · 2020
Cited alongside, same era.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Cited alongside, same era.
Improved protein structure prediction using potentials from deep learning
Andrew W Senior, Richard Evans, John Jumper, James Kirkpatrick, Laurent Sifre, Tim Green, Chongli Qin, Augustin Žídek, Alexander WR Nelson, Alex Bridgland, et al · 2020
Cited alongside, same era.
First neural conjecturing datasets and experiments
Josef Urban and Jan Jakubŭv · 2020
Cited alongside, same era.
Learning to prove theorems by learning to generate theorems
Mingzhe Wang and Jia Deng · 2020
Cited alongside, same era.
Later among the works it cites.
Star: Bootstrapping reasoning with reasoning
Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman · 2022
Later among the works it cites.
Llemma: An open language model for mathematics
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck · 2023
Later among the works it cites.
Language models can teach themselves to program better
Patrick Haluptzok, Matthew Bowers, and Adam Tauman Kalai · 2023
Later among the works it cites.
Large language models can self-improve
Jiaxin Huang, Shixiang Gu, Le Hou, Yuexin Wu, Xuezhi Wang, Hongkun Yu, and Jiawei Han · 2023
Later among the works it cites.
Peano: learning formal mathematical reasoning
Gabriel Poesia and Noah D Goodman · 2023
Later among the works it cites.
Codeplay: Autotelic learning through collaborative self-play in programming environments
Laetitia Teodorescu, Cédric Colas, Matthew Bowers, Thomas Carta, and Pierre-Yves Oudeyer · 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 J Prenger, and Animashree Anandkumar · 2023
Later among the works it cites.
Machine learning and information theory concepts towards an ai mathematician
Yoshua Bengio and Nikolay Malkin · 2024
Closest in time.
Duper: A proof-producing superposition theorem prover for dependent type theory
Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad · 2024
Closest in time.
Solving olympiad geometry without human demonstrations
Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong · 2024
Closest in time.