Fetching the paper…
Reading the bibliography…
We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems.
Empirical explorations of the logic theory machine: a case study in heuristic
Allen Newell, John Clifford Shaw, and Herbert A Simon · 1957
Earlier work this paper cites.
The William Lowell Putnam Mathematical Competition: Problems and Solutions, 1965-1984
G.L. Alexanderson, L.F. Klosinski, and L.C. Larson · 1985
Earlier work this paper cites.
Isabelle: A generic theorem prover
Lawrence C Paulson · 1994
Earlier work this paper cites.
The four-colour theorem
Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas · 1997
Earlier work this paper cites.
The William Lowell Putnam Mathematical Competition 1985-2000: Problems, Solutions and Commentary
K.S. Kedlaya, B. Poonen, R. Vakil, and Mathematical Association of America · 2002
Earlier work this paper cites.
The isabelle framework
Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow · 2008
Earlier work this paper cites.
Formal verification of a realistic compiler
Xavier Leroy · 2009
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, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry · 2013
Earlier work this paper cites.
Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, 02 2015
Lawrence Paulson and Jasmin Blanchette · 2015
Earlier work this paper cites.
Verdi: a framework for implementing and formally verifying distributed systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson · 2015
Earlier work this paper cites.
Hammer for coq: Automation for dependent type theory
Łukasz Czajka and Cezary Kaliszyk · 2018
Earlier work this paper cites.
Metamath: A Computer Language for Pure Mathematics , 2019
Norman D. Megill and David A. Wheeler · 2019
Earlier work this paper cites.
Learning to prove theorems via interacting with proof assistants
Kaiyu Yang and Jia Deng · 2019
Earlier work this paper cites.
The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq , pp. 271–277
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers · 2020
Earlier work this paper cites.
The William Lowell Putnam Mathematical Competition 2001–2016: Problems, Solutions, and Commentary
K.S. Kedlaya, D.M. Kane, J.M. Kane, and E.M. O’Dorney · 2020
Earlier work this paper cites.
The lean mathematical library
The mathlib Community · 2020
Earlier work this paper cites.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Earlier work this paper cites.
Generating correctness proofs with neural networks
Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner · 2020
Earlier work this paper cites.
Training verifiers to solve math word problems, 2021
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman · 2021
Cited alongside, same era.
Measuring mathematical problem solving with the math dataset, 2021
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt · 2021
Cited alongside, same era.
Lisa: Language models of isabelle proofs, 2021
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Cited alongside, same era.
The lean 4 theorem prover and programming language
Leonardo de Moura and Sebastian Ullrich · 2021
Cited alongside, same era.
Online machine learning techniques for coq: A comparison, 2021
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Černý, Cezary Kaliszyk, and Josef Urban · 2021
Cited alongside, same era.
Archive of Formal Proofs — isa-afp.org
AFP · 2024
Closest in time.
Llemma: An Open Language Model For Mathematics, 2024
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck · 2024
Closest in time.
Graph2tac: Online representation learning of formal math concepts, 2024
Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun · 2024
Closest in time.
IMO Grand Challenge — imo-grand-challenge.github.io
IMO Grand Challenge · 2024
Closest in time.
William Lowell Putnam Mathematical Competition | Mathematical Association of America — maa.org
William-Lowell Putnam Mathematical Competition · 2024
Closest in time.
GitHub - dwrensha/compfiles: Catalog Of Math Problems Formalized In Lean — github.com
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2021
Cited alongside, same era.
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
Cited alongside, same era.
Formal mathematics statement curriculum learning, 2022
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever · 2022
Cited alongside, same era.
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad · 2023
Cited alongside, same era.
Baldur: whole-proof generation and repair with large language models
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun · 2023
Cited alongside, same era.
Fimo: A challenge formal dataset for automated theorem proving, 2023
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu · 2023
Cited alongside, same era.
Gpt-4 technical report, 2023
OpenAI · 2023
Cited alongside, same era.
Compfiles · 2024
Closest in time.
Coquelicot
Coquelicot · 2024
Closest in time.
GitHub - GeoCoq/GeoCoq: A formalization of geometry in Coq based on Tarski’s axiom system — github.com
GeoCoq · 2024
Closest in time.
A survey on deep learning for theorem proving, 2024
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si · 2024
Closest in time.
GitHub - math-comp/math-comp: Mathematical Components — github.com
Mathcomp · 2024
Closest in time.
GitHub - math-comp/analysis: Mathematical Components compliant Analysis Library — github.com
mathcomp-analysis · 2024
Closest in time.
AIMO Prize — aimoprize.com
Prize · 2024
Closest in time.
An In-Context Learning Agent for Formal Theorem-Proving
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri · 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.
GitHub - rahul3613/ProofNet-lean4: ProofNet dataset ported into Lean 4 — github.com
Rahul Vishwakarma, Pietro Monticone, and Abhijit Niser · 2024
Closest in time.
Proving theorems recursively, 2024
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, and Xiaodan Liang · 2024
Closest in time.
Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data, 2024
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang · 2024
Closest in time.