Communities
Connect sessions
AI calendar
Organizations
Join Slack
Contact Sales
Search
Open menu
Home
Papers
2408.03350
Cited By
v1
v2
v3 (latest)
miniCTX: Neural Theorem Proving with (Long-)Contexts
International Conference on Learning Representations (ICLR), 2024
5 August 2024
Jiewen Hu
Thomas Zhu
Sean Welleck
AIMat
Re-assign community
ArXiv (abs)
PDF
HTML
HuggingFace (1 upvotes)
Github (194★)
Papers citing
"miniCTX: Neural Theorem Proving with (Long-)Contexts"
35 / 35 papers shown
miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
Azim Ospanov
Farzan Farnia
Roozbeh Yousefzadeh
219
1
0
05 Nov 2025
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
Jiedong Jiang
Wanyi He
Yuefeng Wang
Guoxiong Gao
Yongle Hu
...
Nailing Guan
Peihao Wu
Chunbo Dai
Liang Xiao
Bin Dong
AIMat
ELM
LRM
514
12
0
04 Nov 2025
RLMEval: Evaluating Research-Level Neural Theorem Proving
Auguste Poiroux
Antoine Bosselut
Viktor Kuncak
AIMat
OffRL
349
2
0
29 Oct 2025
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
Xiao-Wen Yang
Zihao Zhang
Jianuo Cao
Zhi Zhou
Zenan Li
Lan-Zhe Guo
Yuan Yao
Taolue Chen
Yu-Feng Li
Xiaoxing Ma
ALM
LRM
179
2
0
26 Sep 2025
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
L. Chen
J. Gu
Daigang Xu
Wenhao Huang
Z. L. Jiang
...
Ge Zhang
Tianyun Zhao
Jianqiu Zhao
Yichi Zhou
Thomas Hanwen Zhu
AIMat
LRM
311
64
0
31 Jul 2025
Premise Selection for a Lean Hammer
Thomas Zhu
Joshua Clune
Jeremy Avigad
Albert Qiaochu Jiang
Sean Welleck
234
6
0
09 Jun 2025
Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening
Andre He
Daniel Fried
Sean Welleck
452
45
0
03 Jun 2025
CLEVER: A Curated Benchmark for Formally Verified Code Generation
Amitayush Thakur
Jasper Lee
George Tsoukalas
Meghana Sistla
Matthew Zhao
Stefan Zetzsche
Greg Durrett
Yisong Yue
Swarat Chaudhuri
ALM
572
23
0
20 May 2025
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Azim Ospanov
Farzan Farnia
Roozbeh Yousefzadeh
LRM
622
15
0
09 May 2025
APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
Huajian Xin
Luming Li
Xiaoran Jin
Jacques Fleuriot
Wenda Li
AIMat
371
3
0
27 Apr 2025
Programming with Pixels: Can Computer-Use Agents do Software Engineering?
Pranjal Aggarwal
Sean Welleck
480
1
0
24 Feb 2025
Formal Mathematical Reasoning: A New Frontier in AI
Kaiyu Yang
Gabriel Poesia
Jingxuan He
Wenda Li
Kristin Lauter
Swarat Chaudhuri
Dawn Song
LRM
AI4CE
626
78
0
20 Dec 2024
ImProver: Agent-Based Automated Proof Optimization
International Conference on Learning Representations (ICLR), 2024
Riyaz Ahuja
Jeremy Avigad
Prasad Tetali
Sean Welleck
LLMAG
379
3
0
07 Oct 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Huajian Xin
Zhaochun Ren
Junxiao Song
Zhihong Shao
Wanjia Zhao
...
Dejian Yang
Zhibin Gou
Z. F. Wu
Fuli Luo
Chong Ruan
AIMat
LRM
370
154
0
15 Aug 2024
Reliable Evaluation and Benchmarks for Statement Autoformalization
Auguste Poiroux
Gail Weiss
Viktor Kuncak
Antoine Bosselut
521
10
0
11 Jun 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Peiyang Song
Kaiyu Yang
A. Anandkumar
455
10
0
18 Apr 2024
InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning
Huaiyuan Ying
Shuo Zhang
Linyang Li
Zhejian Zhou
Yunfan Shao
...
Hang Yan
Xipeng Qiu
Jiayu Wang
Kai-xiang Chen
Dahua Lin
ReLM
LRM
276
125
0
09 Feb 2024
DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence
Daya Guo
Qihao Zhu
Dejian Yang
Zhenda Xie
Kai Dong
...
Yu-Huan Wu
Yiming Li
Fuli Luo
Yingfei Xiong
W. Liang
ELM
526
1,565
0
25 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts
Lasse Blaauwbroek
Miroslav Olšák
Jason Rute
F. I. S. Massolo
Jelle Piepenbrock
Vasily Pestun
324
18
0
05 Jan 2024
LLMSTEP: LLM proofstep suggestions in Lean
Sean Welleck
Rahul Saha
282
39
0
27 Oct 2023
Llemma: An Open Language Model For Mathematics
International Conference on Learning Representations (ICLR), 2023
Zhangir Azerbayev
Hailey Schoelkopf
Keiran Paster
Marco Dos Santos
Alexander Shmakov
Albert Q. Jiang
Jia Deng
Stella Biderman
Sean Welleck
CLL
487
424
0
16 Oct 2023
FIMO: A Challenge Formal Dataset for Automated Theorem Proving
Chengwu Liu
Jianhao Shen
Huajian Xin
Zhengying Liu
Ye Yuan
...
Chuanyang Zheng
Yichun Yin
Lin Li
Ming Zhang
Qun Liu
AIMat
AI4CE
315
52
0
08 Sep 2023
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Neural Information Processing Systems (NeurIPS), 2023
Kaiyu Yang
Aidan M. Swope
Alex Gu
Rahul Chalamala
Peiyang Song
Shixing Yu
Saad Godil
R. Prenger
Anima Anandkumar
RALM
491
404
0
27 Jun 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models
E. First
M. Rabe
Talia Ringer
Yuriy Brun
368
155
0
08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection
International Conference on Learning Representations (ICLR), 2023
Maciej Mikuła
Szymon Tworkowski
Szymon Antoniak
Bartosz Piotrowski
Albert Qiaochu Jiang
Jinyi Zhou
Christian Szegedy
Lukasz Kuciñski
Piotr Milo's
Yuhuai Wu
358
62
0
08 Mar 2023
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
Zhangir Azerbayev
Bartosz Piotrowski
Hailey Schoelkopf
Edward W. Ayers
Dragomir R. Radev
J. Avigad
AIMat
242
144
0
24 Feb 2023
A Survey of Deep Learning for Mathematical Reasoning
Annual Meeting of the Association for Computational Linguistics (ACL), 2022
Pan Lu
Liang Qiu
Wenhao Yu
Sean Welleck
Kai-Wei Chang
ReLM
LRM
402
194
0
20 Dec 2022
Towards a Mathematics Formalisation Assistant using Large Language Models
Ayush Agrawal
Siddhartha Gadgil
Navin Goyal
Ashvni Narayanan
Anand Tadipatri
254
22
0
14 Nov 2022
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
International Conference on Learning Representations (ICLR), 2022
Albert Q. Jiang
Sean Welleck
Jin Peng Zhou
Wenda Li
Hamish Ivison
M. Jamnik
Timothée Lacroix
Yuhuai Wu
Guillaume Lample
AIMat
383
273
0
21 Oct 2022
HyperTree Proof Search for Neural Theorem Proving
Neural Information Processing Systems (NeurIPS), 2022
Guillaume Lample
Marie-Anne Lachaux
Thibaut Lavril
Xavier Martinet
Amaury Hayat
Gabriel Ebner
Aurelien Rodriguez
Timothée Lacroix
AIMat
453
207
0
23 May 2022
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Neural Information Processing Systems (NeurIPS), 2022
Albert Q. Jiang
Wenda Li
Szymon Tworkowski
K. Czechowski
Tomasz Odrzygó'zd'z
Piotr Milo's
Yuhuai Wu
M. Jamnik
AIMat
LRM
277
129
0
22 May 2022
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
International Conference on Learning Representations (ICLR), 2021
Kunhao Zheng
Jesse Michael Han
Stanislas Polu
AIMat
668
327
0
31 Aug 2021
Proof Artifact Co-training for Theorem Proving with Language Models
International Conference on Learning Representations (ICLR), 2021
Jesse Michael Han
Jason M. Rute
Yuhuai Wu
Edward W. Ayers
Stanislas Polu
AIMat
565
148
0
11 Feb 2021
Learning to Prove Theorems via Interacting with Proof Assistants
International Conference on Machine Learning (ICML), 2019
Kaiyu Yang
Gaowen Liu
AIMat
LRM
461
173
0
21 May 2019
DeepMath - Deep Sequence Models for Premise Selection
Alexander A. Alemi
François Chollet
N. Eén
G. Irving
Christian Szegedy
Josef Urban
LRM
AIMat
340
254
0
14 Jun 2016
1
Page 1 of 1
