Fetching the paper…
Reading the bibliography…
Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems.
A Computer Program for Presburger’s Algorithm
Martin Davis · 1957
Earlier work this paper cites.
A Computing Procedure for Quantification Theory
Martin Davis and Hilary Putnam · 1960
Earlier work this paper cites.
The Mathematical Language Automath, Its Usage and Some of Its Extensions
N.G. Bruijn, de · 1970
Earlier work this paper cites.
Implementation and Applications of Scott’s Logic for Computable Functions
Robin Milner · 1972
Earlier work this paper cites.
Automatic Acquisition of Search Guiding Heuristics
Christian Suttner and Wolfgang Ertel · 1990
Earlier work this paper cites.
Cones of Matrices and Set-Functions and 0–1 Optimization
László Lovász and Alexander Schrijver · 1991
Earlier work this paper cites.
An Overview of the Mizar Project
Piotr Rudnicki · 1992
Earlier work this paper cites.
Isabelle: A Generic Theorem Prover
Lawrence C Paulson · 1994
Earlier work this paper cites.
HOL Light: A Tutorial Introduction
John Harrison · 1996
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.
Learning from Previous Proof Experience: A Survey
Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz · 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.
Policy Gradient Methods for Reinforcement Learning with Function Approximation
Richard S Sutton, David McAllester, Satinder Singh, and Yishay Mansour · 1999
Earlier work this paper cites.
A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering
Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang · 2000
Earlier work this paper cites.
Automated Theorem Proving in Software Engineering
Johann M Schumann · 2001
Earlier work this paper cites.
BLEU: A Method for Automatic Evaluation of Machine Translation
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu · 2002
Earlier work this paper cites.
E–A Brainiac Theorem Prover
Stephan Schulz · 2002
Earlier work this paper cites.
An Extensible SAT-Solver
Niklas Eén and Niklas Sörensson · 2003
Earlier work this paper cites.
leanCoP: Lean Connection-Based Theorem Proving
Jens Otten and Wolfgang Bibel · 2003
Earlier work this paper cites.
Z3: An efficient SMT solver
Leonardo De Moura and Nikolaj Bjørner · 2008
Earlier work this paper cites.
The Four Colour Theorem: Engineering of a Formal Proof
Georges Gonthier · 2008
Earlier work this paper cites.
iProver–An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Konstantin Korovin · 2008
Earlier work this paper cites.
seL4: Formal Verification of an OS Kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al · 2009
Earlier work this paper cites.
The Probabilistic Relevance Framework: BM25 and Beyond
Stephen Robertson, Hugo Zaragoza, et al · 2009
Earlier work this paper cites.
Sledgehammer: Judgement Day
Sascha Böhme and Tobias Nipkow · 2010
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.
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes · 2012
Earlier work this paper cites.
First-Order Theorem Proving and Vampire
Laura Kovács and Andrei Voronkov · 2013
Earlier work this paper cites.
Playing Atari with Deep Reinforcement Learning
Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin Riedmiller · 2013
Earlier work this paper cites.
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014
Earlier work this paper cites.
Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation
Kyunghyun Cho, Bart Van Merriënboer, Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Holger Schwenk, and Yoshua Bengio · 2014
Earlier work this paper cites.
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
Cezary Kaliszyk, Josef Urban, Jiří Vyskočil, and Herman Geuvers · 2014
Earlier work this paper cites.
Sequence to Sequence Learning with Neural Networks
Ilya Sutskever, Oriol Vinyals, and Quoc V Le · 2014
Earlier work this paper cites.
Convolutional Networks on Graphs for Learning Molecular Fingerprints
David K Duvenaud, Dougal Maclaurin, Jorge Iparraguirre, Rafael Bombarell, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P Adams · 2015
Earlier work this paper cites.
Learning to Parse on Aligned Corpora (Rough Diamond)
Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil · 2015
Earlier work this paper cites.
Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks
Kai Sheng Tai, Richard Socher, and Christopher D Manning · 2015
Earlier work this paper cites.
Hammering Towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban · 2016
Earlier work this paper cites.
CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo · 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.
CompCert–A Formally Verified Optimizing Compiler
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand · 2016
Earlier work this paper cites.
WaveNet: A Generative Model for Raw Audio
Aaron Van Den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew Senior, Koray Kavukcuoglu, et al · 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, Pieter Abbeel, and Wojciech Zaremba · 2017
Earlier work this paper cites.
A Formal Proof of the Kepler Conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al · 2017
Earlier work this paper cites.
ENIGMA: Efficient Learning-Based Inference Guiding Machine
Jan Jakubüv and Josef Urban · 2017
Earlier work this paper cites.
HolStep: A Machine Learning Dataset for Higher-Order Logic Theorem Proving
Cezary Kaliszyk, François Chollet, and Christian Szegedy · 2017
Earlier work this paper cites.
Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Earlier work this paper cites.
Neural Machine Translation (seq2seq) Tutorial
Minh-Thang Luong, Eugene Brevdo, and Rui Zhao · 2017
Earlier work this paper cites.
Tree-Structure CNN for Automated Theorem Proving
Kebin Peng and Dianfu Ma · 2017
Earlier work this paper cites.
The TPTP Problem Library and Associated Infrastructure
Geoff Sutcliffe · 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
Earlier work this paper cites.
Premise Selection for Theorem Proving by Deep Graph Embedding
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng · 2017
Earlier work this paper cites.
Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka and Cezary Kaliszyk · 2018
Earlier work this paper cites.
Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák · 2018
Earlier work this paper cites.
Premise Selection with Neural Networks and Distributed Representation of Features
Andrzej Stanisław Kucik and Konstantin Korovin · 2018
Earlier work this paper cites.
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai · 2018
Earlier work this paper cites.
Phrase-Based & Neural Unsupervised Machine Translation
Guillaume Lample, Myle Ott, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato · 2018
Earlier work this paper cites.
Representation Learning with Contrastive Predictive Coding
Aaron van den Oord, Yazhe Li, and Oriol Vinyals · 2018
Earlier work this paper 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, et al · 2018
Earlier work this paper cites.
Graph Attention Networks
Petar Veličković, Guillem Cucurull, Arantxa Casanova, Adriana Romero, Pietro Lio, and Yoshua Bengio · 2018
Earlier work this paper cites.
First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban · 2018
Earlier work this paper cites.
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving
Kshitij Bansal, Sarah M. Loos, Markus Norman Rabe, Christian Szegedy, and Stewart Wilcox · 2019
Earlier work this paper cites.
CaDiCaL at the SAT Race 2019
Armin Biere · 2019
Earlier work this paper cites.
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Karel Chvalovskỳ, Jan Jakubüv, Martin Suda, and Josef Urban · 2019
Earlier work this paper cites.
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
Maxwell Crouse, Ibrahim Abdelaziz, Cristina Cornelio, Veronika Thost, Lingfei Wu, Kenneth Forbus, and Achille Fokoue · 2019
Earlier work this paper cites.
BERT: Pre-Training of Deep Bidirectional Transformers for Language Understanding
Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova · 2019
Earlier work this paper cites.
Learning Dynamic Polynomial Proofs
Alhussein Fawzi, Mateusz Malinowski, Hamza Fawzi, and Omar Fawzi · 2019
Earlier work this paper cites.
Learning Representations of Logical Formulae using Graph Neural Networks
Xavier Glorot, Ankit Anand, Eser Aygun, Shibl Mourad, Pushmeet Kohli, and Doina Precup · 2019
Earlier work this paper cites.
Usefulness of Lemmas via Graph Neural Networks
Zarathustra A Goertzel and Josef Urban · 2019
Earlier work this paper cites.
GamePad: A Learning Environment for Theorem Proving
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever · 2019
Earlier work this paper cites.
Hammering Mizar by Learning Clause Guidance
Jan Jakubüv and Josef Urban · 2019
Earlier work this paper cites.
Cross-Lingual Language Model Pretraining
Guillaume Lample and Alexis Conneau · 2019
Earlier work this paper cites.
RoBERTa: A Robustly Optimized BERT Pretraining Approach
Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov · 2019
Earlier work this paper cites.
Metamath: A Computer Language for Mathematical Proofs
Norman Megill and David A Wheeler · 2019
Earlier work this paper cites.
Property Invariant Embedding for Automated Reasoning
Miroslav Olšák, Cezary Kaliszyk, and Josef Urban · 2019
Cited alongside, same era.
A Neurally-Guided, Parallel Theorem Prover
Michael Rawson and Giles Reger · 2019
Cited alongside, same era.
How Powerful are Graph Neural Networks?
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka · 2019
Cited alongside, same era.
Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang and Jia Deng · 2019
Cited alongside, same era.
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
Ibrahim Abdelaziz, Veronika Thost, Maxwell Crouse, and Achille Fokoue · 2020
Cited alongside, same era.
Autoformalization with Large Language Models
Yuhuai Wu, Albert Q Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy · 2022
Later among the works it cites.
ByT5: Towards a Token-Free Future with Pre-trained Byte-to-Byte Models
Linting Xue, Aditya Barua, Noah Constant, Rami Al-Rfou, Sharan Narang, Mihir Kale, Adam Roberts, and Colin Raffel · 2022
Later among the works it cites.
Generating Natural Language Proofs with Verifier-Guided Search
Kaiyu Yang, Jia Deng, and Danqi Chen · 2022
Later among the works it cites.
MiniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu · 2022
Later among the works it cites.
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al · 2023
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, and Shibl Mourad · 2020
Cited alongside, same era.
Learning Alignment between Formal & Informal Mathematics
Kshitij Bansal and Christian Szegedy · 2020
Cited alongside, same era.
Language Models are Few-Shot Learners
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al · 2020
Cited alongside, same era.
A Simple Framework for Contrastive Learning of Visual Representations
Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey Hinton · 2020
Cited alongside, same era.
Transformers as Soft Reasoners over Language
Peter Clark, Oyvind Tafjord, and Kyle Richardson · 2020
Cited alongside, same era.
TacTok: Semantics-Aware Proof Synthesis
Emily First, Yuriy Brun, and Arjun Guha · 2020
Cited alongside, same era.
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
Thibault Gauthier · 2020
Cited alongside, same era.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad · 2023
Later among the works it cites.
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
Filip Bártek and Martin Suda · 2023
Later among the works it cites.
MLFMF: Data Sets for Machine Learning for Mathematical Formalization
Andrej Bauer, Matej Petković, and Ljupco Todorovski · 2023
Later among the works it cites.
PaLM: Scaling Language Modeling with Pathways
Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al · 2023
Later among the works it cites.
Guiding an Instantiation Prover with Graph Neural Networks
Karel Chvalovskỳ, Konstantin Korovin, Jelle Piepenbrock, and Josef Urban · 2023
Later among the works it cites.
Evaluating Language Models for Mathematics through Interactions
Katherine M Collins, Albert Q Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B Tenenbaum, William Hart, et al · 2023
Later among the works it cites.
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun · 2023
Later among the works it cites.
An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations
Achille Fokoue, Ibrahim Abdelaziz, Maxwell Crouse, Shajith Ikbal, Akihiro Kishimoto, Guilherme Lima, Ndivhuwo Makondo, and Radu Marinescu · 2023
Later among the works it cites.
Temperature-Scaled Large Language Models for Lean Proofstep Prediction
Fabian Gloeckle, Baptiste Roziere, Amaury Hayat, and Gabriel Synnaeve · 2023
Later among the works it cites.
Graph Sequence Learning for Premise Selection
Edvard K Holden and Konstantin Korovin · 2023
Later among the works it cites.
MizAR 60 for Mizar 50
Jan Jakubüv, Karel Chvalovskỳ, Zarathustra A Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban · 2023
Later among the works it cites.
Exploring Mathematical Conjecturing with Large Language Models
Moa Johansson and Nicholas Smallbone · 2023
Later among the works it cites.
Finding Inductive Loop Invariants using Large Language Models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma · 2023
Later among the works it cites.
Math Education with Large Language Models: Peril or Promise?
Harsh Kumar, David M Rothschild, Daniel G Goldstein, and Jake M Hofman · 2023
Later among the works it cites.
BERT Is Not The Count: Learning to Match Mathematical Statements with Proofs
Weixian Waylon Li, Yftah Ziser, Maximin Coavoux, and Shay B Cohen · 2023
Later among the works it cites.
UniMath: A Foundational and Multimodal Mathematical Reasoner
Zhenwen Liang, Tianyu Yang, Jipeng Zhang, and Xiangliang Zhang · 2023
Later among the works it cites.
FIMO: A Challenge Formal Dataset for Automated Theorem Proving
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al · 2023
Later among the works it cites.
Reinforcement Learning for Guiding the E Theorem Prover
Jack McKeown and Geoff Sutcliffe · 2023
Later among the works it cites.
Learning Deductive Reasoning from Synthetic Corpus based on Formal Logic
Terufumi Morishita, Gaku Morio, Atsuki Yamaguchi, and Yasuhiro Sogawa · 2023
Later among the works it cites.
LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers
Theo X Olausson, Alex Gu, Benjamin Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger Levy · 2023
Later among the works it cites.
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang · 2023
Later among the works it cites.
A New Approach Towards Autoformalization
Nilay Patel, Jeffrey Flanigan, and Rahul Saha · 2023
Later among the works it cites.
Can Large Language Models Reason about Program Invariants?
Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin · 2023
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 · 2023
Later among the works it cites.
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
Tom Reichel, R Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer · 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.
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought
Abulhair Saparov and He He · 2023
Later among the works it cites.
Experimental Results from Applying GPT-4 to An Unpublished Formal Language
Gregor vom Scheidt · 2023
Later among the works it cites.
gym-saturation: Gymnasium Environments for Saturation Provers (System description)
Boris Shminke · 2023
Later among the works it cites.
Clover: Closed-Loop Verifiable Code Generation
Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett · 2023
Later among the works it cites.
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
Rahul Vishwakarma and Subhankar Mishra · 2023
Later among the works it cites.
LLMSTEP: LLM Proofstep Suggestions in Lean
Sean Welleck and Rahul Saha · 2023
Later among the works it cites.
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, et al · 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.
Leveraging Large Language Models for Automated Proof Synthesis in Rust
Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui · 2023
Later among the works it cites.
SATLM: Satisfiability-Aided Language Models using Declarative Prompting
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett · 2023
Later among the works it cites.
CoProver: A Recommender System for Proof Construction
Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, and Natarajan Shankar · 2023
Later among the works it cites.
Large Language Models’ Understanding of Math: Source Criticism and Extrapolation
Roozbeh Yousefzadeh and Xuenan Cao · 2023
Later among the works it cites.
Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, and Jingbo Shang · 2024
Closest in time.
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 · 2024
Closest in time.
Machine Learning and Information Theory Concepts Towards an AI Mathematician
Yoshua Bengio and Nikolay Malkin · 2024
Closest in time.
Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search
David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge, Jianang Yang, Simon Henniger, William E Byrd, Robert Zinkov, and Nada Amin · 2024
Closest in time.
Lean in 2024
Kevin Buzzard · 2024
Closest in time.
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu Lahiri, and Nikhil Swamy · 2024
Closest in time.
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang · 2024
Closest in time.
LeanReasoner: Boosting Complex Logical Reasoning with Lean
Dongwei Jiang, Marcio Fonseca, and Shay B Cohen · 2024
Closest in time.
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, and Paul Montague · 2024
Closest in time.
miniCodeProps: A Minimal Benchmark for Proving Code Properties
Evan Lohn and Sean Welleck · 2024
Closest in time.
Process-Driven Autoformalization in Lean 4
Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo · 2024
Closest in time.
Magnushammer: A Transformer-Based Approach to Premise Selection
Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Q Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu · 2024
Closest in time.
Autoformalizing Euclidean Geometry
Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si · 2024
Closest in time.
OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text
Keiran Paster, Marco Dos Santos, Zhangir Azerbayev, and Jimmy Ba · 2024
Closest in time.
Learning formal mathematics from intrinsic motivation
Gabriel Poesia, David Broman, Nick Haber, and Noah D Goodman · 2024
Closest in time.
Improving Autoformalization using Type Checking
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut · 2024
Closest in time.
Solving Proof Block Problems Using Large Language Models
Seth Poulsen, Sami Sarsa, James Prather, Juho Leinonen, Brett A Becker, Arto Hellas, Paul Denny, and Brent N Reeves · 2024
Closest in time.
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
Xin Quan, Marco Valentino, Louise A Dennis, and André Freitas · 2024
Closest in time.
Graph2Tac: Online Representation Learning of Formal Math Concepts
Jason Rute, Miroslav Olšák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun · 2024
Closest in time.
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models
Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo · 2024
Closest in time.
Towards Large Language Models as Copilots for Theorem Proving in Lean
Peiyang Song, Kaiyu Yang, and Anima Anandkumar · 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.
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri · 2024
Closest in time.
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al · 2024
Closest in time.
Proving Olympiad Algebraic Inequalities without Human Demonstrations
Chenrui Wei, Mengzhou Sun, and Wei Wang · 2024
Closest in time.
Lean-github: Compiling github lean repositories for a versatile lean prover
Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen · 2024
Closest in time.
Selene: Pioneering Automated Proof in Software Verification
Lichen Zhang, Shuai Lu, and Nan Duan · 2024
Closest in time.
Subgoal-Based Demonstration Learning for Formal Theorem Proving
Xueliang Zhao, Wenda Li, and Lingpeng Kong · 2024
Closest in time.
Lyra: Orchestrating Dual Correction in Automated Theorem Proving
Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li · 2024
Closest in time.