miniCTX: Neural Theorem Proving with (Long-)Contexts
Authors: Jiewen Hu
Thomas Zhu
Sean Welleck
Venue: ICLR 2025 Oral (2025)
Keywords: Neural theorem proving
Formal mathematics
Benchmark dataset
Primary area: datasets and benchmarks
TL;DR: We introduce a context-rich dataset and toolkit for evaluation of neural theorem proving under a more realistic scenario.

Abstract: Real-world formal theorem proving often depends on a wealth of context, including definitions, lemmas, comments, file structure, and other information. We introduce $\texttt{miniCTX}$, which tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. $\texttt{miniCTX}$ contains theorems sourced from real Lean projects and textbooks, each associated with a context that can span tens of thousands of tokens. Models are tasked with proving a theorem given access to code from the theorem's repository, which contains context that is needed for the proof. As a baseline for $\texttt{miniCTX}$, we tested fine-tuning and prompting methods that condition theorem proving on preceding context. Both approaches substantially outperform traditional methods that rely solely on state information. We found that this ability to use context is not captured by previous benchmarks such as $\texttt{miniF2F}$. Alongside $\texttt{miniCTX}$, we offer $\texttt{ntp-toolkit}$ for automatically extracting and annotating theorem proving data, making it easy to add new projects into $\texttt{miniCTX}$ to ensure that contexts are not seen during training. $\texttt{miniCTX}$ offers a challenging and realistic evaluation of neural theorem provers.

Published as a conference paper at ICLR 2025
MINICTX: NEURAL THEOREM PROVING WITH (LONG-) CONTEXTS
Jiewen Hu Thomas Zhu Carnegie Mellon University
Sean Welleck
ABSTRACT
Real-world formal theorem proving often depends wealth of context, including definitions, lemmas, comments, file structure, and other information. We introduce miniCTX, which tests model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. miniCTX contains theorems sourced from real Lean projects and textbooks, each associated with context that can span tens of thousands of tokens. Models are tasked with proving a theorem given access to code from the theorem's repository, which contains context that is needed for the proof. As baseline for miniCTX, we tested fine-tuning and prompting methods that condition theorem proving on preceding context. Both approaches substantially outperform traditional methods that rely solely on state information. We found that this ability to use context is not captured by previous benchmarks such as miniF2F. Alongside miniCTX, we offer NTP-TOOLKK for automatically extracting and annotating theorem proving data, making it easy to add new projects into miniCTX to ensure that contexts are not seen during training. miniCTX offers a challenging and realistic evaluation of neural theorem provers
INTRODUCTION
Formal theorem proving in interactive theorem provers (ITPs) provides a testbed for evaluating the reasoning capabilities of large language models (LL.Ms). Theorem proving capabilities can then directly translate to automation for mathematicians, such via tools that complete formalize proofs (Welleck Saha, 2023] Song et al. 2024, Welleck] 2024 AAgawal et al. 2022). However, despite their promise, and the complexity of real-world theorem proving.
gap between the evaluation of current language model-based provers
Our motivating observation is that theorems and proofs depend on various forms of context, such as newly-define definitions and lemmas. For instance, to prove results about a square, one might first formalize definition of rectangle, prove some results about rectangles, then specialize them to newly-defined square (Kontorovich) 2024b) (Figure T). However, existing methods for training and evaluating LLM-based theorem provers often fail to incorporate the full range of contextual information available in real-world projects. For example, benchmarks often focus on proving standalone competition problems (e.g., miniF2F (Zheng et al.) (0022) or theorems from a library that the model has trained on (e.g.. Mathlib (Han et al. [022]] Yang et al. (203)). and state-of ofate-of-the-are ttthhharr art LLM-based provers are trained to accept only a proof state as input, making them unaware of new theorems and definitions (Polu & Sutskever] 2020 Ying et al. 2024, Xin et al. 2024). While some existing work, including premise selection techniques Jiang et al. 20222] Mikula et al. 2023] Yang al. 2023) and datasets like CogGym (Yang & Deng 2019), have explored theorem proving based on information beyond the current state, they often focus only on providing relevant premises premises-lemmee lemmas
that can assist proof construction which only subset of the available information.
Building on these foundations, we propose miniCTX: a benchmark that seeks to expand the scope of context used in theorem proving. We extend beyond traditional premise selection explored in prior benchmarks (e.g., Yang et al. (203);; Yang & Deng (2019) by incorporating a more comprehensive set of contextual elements. This includes premises, prior proofs, comments, notation, and structural
Projecc page: https://cmmu 13. 1.s.gittubb... io/minictx Please refer to our project page for our dataset. and evaluation links, and future updates including miniCTX-v2.

---

Published as conference paper at ICLR 2025
Table 1: Comparison of theorem proving benchmarks across several key features.
Benchmark
Language
Premise
Full Context
Multi-source
Temporal Split
miniF2F Zheng et 2022
Multiple
ProofNet Azerbayev et al.
2023
Lean
LeanDojo
Tang et al. 2023
X
LeanStep
Han ot al. 2022
Lean
X
X
CoqGym
Yang & Deng 2019
Coq
X
X
PISA (Jiang et al 2021
Isabelle
X
X
miniCIX (Ours)
Lean
components like imports and declarations. By doing so, miniCTX aims to drive the development of methods that understand and work with context that occurs in complex, real-world theorem proving tasks. We compare miniCTT miCTX with several popular theorem proving datasets to highlight its unique contributions in terms of contextual dependency and real-world applicability (see Table I. Additionally, considering the common use of pre-trained language models we mitigate potential data contamination by continually and automatically updating miniCTX with new Lean projects, that evaluated theorems are not seen during training. Our key contributions are:
miniCTX Benchmark: We introduce miniCTX, the first benchmark designed specifically to evaluate theorem proving in real-world settings where proofs depend on in-file definitions, lemmas, and context from formal projects. miniCTX presents unique challenge by requiring models to reason over long contexts and handle dependencies that arise real-world theorem proving tasks.
NOO-IOOLKIT:
To facilitate the automatic updating of miniCTX, developed the NTP-TOOLKIT, which automatically extracts relevant theorems and contexts from Lean projects. Additionally, we provide Lean REPL wrapper that enables simpler evaluation miniCTX.
We evaluate miniCTy CTX on several existing baseline models, including different fine-tuning and prompting strategies, as well methods with premise selection. We also propose file- tuning, a strong baseline method for training models using full file contexts, where both the theorem statements and their surrounding context are provided during training. This approach establishes robust baseline for future work on context-dependen theorem proving.
Baseline Evaluations:
Existing Theorews andl Proofs Ceg. Matilks
Existing Theorems and Proofs leg, Matrii)
Train Test
New Formalization Ceg. Prine Rlmber Thgorga)
Standalone test
Dependent test theorem
theeren
Ver dePwition,
Suar (-0) SEAT pEP
Sparr 10:
Traditional
Context- proving
LLM proving
Figure 1: Many state of the art provers are trained on static dataset of theorems and proofs, then evaluated on standalone problems such competition problems (left). We argue that neural provers must also operate in the realistic context-dependent setting, in which results depend on working with new mathematical objects and their facts, notations, and the structural elements the project (imports, variables, etc.) (right).
2 THEOREM PROVING WITH CONTEXT
For language model-based provers to function useful tools in this real-world setting, they need to be able to work with new information such as new definitions or lemmas. For example, a system suggesting proofs in the Prime Number Theorem project should be familiar with the project's
2

---

Published as a conference paper at ICLR 2025
definition of "square". Many current language model-based provers trained on static snapshot of data, and are hence unaware of any context that was created after the model was trained (Figure IT. They are often evaluated on either context-less standalone competition problems (Zheng et al. 2002 Azerbayev et al. 2023) that do not reflect realistic settings, or existing Mathlib proofs (Yang et al. 2023) which risks data contamination. As result, it remains unclear whether these models can work with new information, which is necessary for using them as an assistant in a real proof development, and how enable this capability.
Context-dependent proving, We study context-dependent theorem proving, where the goal is for a model to generate proofs y for new theorems 2, based on context that includes background information such as definitions, lemmas, or natural language comments. Formally, the problem is
(1) where (zz, c) p denotes (theorem, context) pair from context distribution p, M is a model that produces a proof y, and e returns if the proof is correct and otherwise.
maximizess B(g,e))pEEy-M (e..)))))) (z, c,
Evaluating context-dependent proving. We choose Lean (Moura & Ullrich 2021 as the verifier v, because of the large body of recent theorems in Lean that can be used as evaluation data, and the abundance of proving methods in Lean that we as baselines. We treat Lean repository as the distribution Each context is a subset of the repository, including new definitions, lemmas, notations, imports, and comments that are relevant the theorem.
Given a language model, we can test three kinds of generalization by ensuring the following:
Theorem-level generalization: the proof must not occur in the model's training data. Context-level generalization: the code and proof must not oceur the training data.
Project-level generalization: the entire repository must not occur in the training data.
For baseline evaluations, we investigate the in-file context case where is the source code that precedes the theorem x in file, as well as cross-file context where e includes both preceding code and relevant premises retrieved from imported modules through premise selection.
MINICTX: A BENCHMARK FOR THEOREM PROVING WITH CONTEXT
We develop miniCTX, Lean 4 theorem proving benchmark of theorems that depend on newly- defined lemmas, definitions, and proofs from within a project. mini CTX currently based on 762 theorems from six projects: (1) Prime Number Theorem (PNT) (Kontorovich) 2024a). (2) Polynomial
Freiman-Ruzze Conjecture and its extension with high cross-file dependency (PFR) (Too 2023).
(3) recent results from the standard mathematical library (Mathlib), (4) an introductory text theorem proving (HTPI) (Macbeth, 2023), (5) high energy physics formalization in HepLean (HEP) (Tooby-Smin 2024), and (6) scientific computing formalizations (SciLean) (Skfivan 2021). These theorems are equally split into 381 validation and 381 test theorems. Table 2 shows an overview of the dataset. Each theorem in miniCTX consists of the theorem statement, preceding file contents up to the theorem statement, and metadata, in JSON (see A.I
1. Theorem statement,
2. Preceding file contents up to the theorem statement,
3. Metadata, including:
(a) File name,
(b) Project commit and version,
(c) Commit and time at which the theorem and its file added,
(d) Position of the theorem in the file and number of premises preceding it,
(e) Number of in-file premises and cross-file premises used by the statement or proof,
(f) Imported modules (for premise selection support),
(g) Proof length and type.
Using our benchmark, users can easily reconstruct the complete context for each theorem, including both fn-file and cross-file context. The in-file context is provided directly by preceding file contents, while the cross-file context can be reconstructed using the metadata, which includes information on imported modules. We open-source the dataset and evaluation code.
3

---

Published as a conference paper at ICLR 2025
Table 2: Problem statistics in miniF2F Zheng et 2022) and miniCTX.
Split
Problems valid test
Context Size
In-File Premises
Repo. Premises
Proof Size
(tokens)
(premises/ 100 tokens)
(premises / 100 tokens)
(lines)
min1F2F
244 +
153
3.0
PNT
85 85
10,858
1.87
0.30
3.3
PFR
51 + 51
18,059
0.65
1.10
27.2
PFR Mathlib
43 + 43
4,351
0.44
2.75
2.7
MiniCTX
50 + 50
14,440
6.1
HTPI
45 45
65,082
2.85
0.00
10.7
HEP
61
3,585
5.65
4.25
3.1
Scil.ean
46
6,249
2.08
9.72
All
381 + 381
18,690
2.63
8.5
*Only counting library imports and definitions.
'Excluding theorems without proofs.
3.1 MINICTX SOURCES
(Kontorovich) 2024a) is project started in January 2024 that formalizes the prime number theorem in Lean as well as related concepts, such as counter integral rectangles in C. We find the files Rectangle 1ean and Resi suitable for our purpose of testing context-depended preceding file content context, each file is self-contained within the project and contains new definitions (rectangles, squares) and many interdependent lemmas. See A.2 for an illustration of such lemmas.
PNT. PrimeNumberTTherreee
lean theorem proving, especially when we use
PFR. PFR Tao 2023 is a project started in November 2023 that formalizes a proof of the Polynomial Freiman- Ruzsa (PFR) conjecture. We included 51 validation and 51 test theorems from PFR. We find that proofs of theorems in PFR tend to be much more monolithic and longer in length than those Mathlib or other libraries. PFR also defines custom mathematical concepts and notations (such as Ruzsa distance) and proof typically depends on many lemmas in PFR outside the current file.
PFRerossile- PFRersssile an extension of the PFR split, which includes additional problems to further evaluate cross-file dependencies. To evaluate models' performance problems with extensive cross- file dependencies, we added 43 test theorems from Entropy Group and Entropy Kernel. Group, which have the highest cross-file dependencies in the project. These problems contain three times the number of cross-file premises compared to other math splits, making them strong candidate for evaluating a model's ability to utilize cross-file file premises. 43 validation theorems chosen similarly.
Recent Mathlib Commits. Mathlib (Mathlib Community, 2020), is Lean's 's largest community- maintained repository, encompassing wide range of mathematical concepts, programming APIs, models and is frequently
and common tactics. It is commonly used for training theorem-prooe updated with new definitions, theorems, and refactorings. Therefore, to avoid data contamination, included 50 test and 50 validation theorems newly added to Mathlib since March 2024, by filtering recent Mathlib commits ones that only add new theorems. Assuming that the model was trained prior to April 2024, the Mathlib split guarantees the evaluation of theorem-level generalization.
HTPL HTPI contains the Lean code for the book How to Prove (HTPI) (Velleman) 2019), which explains a systematic approach to constructing mathematical proof's with Lean. It covers topics like elementary logic and number theory, and proving techniques like induction. The files in HTPI typically start with basic definitions and lemmas that might be used throughout the entire file, followed by exercises and several example problems. Therefore, models can utilize definitions, lemmas, and proof structures from example problems to solve exercises, making it an effective benchmark for testing context-dependent theorem-proving models.
HEP. HepLean (Tooby-Smith) 2024) is an open-source project that digitalizes definitions, theorems, proofs, and calculations in high energy physics using Lean. HepLean aims to facilitate discovery, automate new findings, verify correctness, and provide educational tools in physics. We selected files from the space and time section, which introduces several new definitions, including 4D Euclidean spacetime models. These files contain high filfil and cross-fit file dependencies, ideal for evaluating context-dependent theorem proving. This split represents an area outside of mathematics, further expanding the generalization of the benchmark.
4

---

Published as a conference paper at ICLR 2025
Recent SciLean Commits. SciLean (Skrivan 2021) is open-source project designed to formalize concepts in scientific computing using Lean 4. SciLean aims to provide formalized tools and frameworks for efficiently representing and proving properties of numerical methods, differential equations, and optimization problems, bridging applied mathematics and computer science. Given Scilean has been created for 3 years and accessed by multiple projects, similar to our Mathlib split, selected 46 test and 46 validation theorems added to SciLean since March 2024 in order to ensure the data more likely unseen for evaluating models. The newly added problems mostly supplements to existing files, so they evaluate the model's 's ability to apply and learn from previous lemmas.
3.2 PROBLEM SELECTION METHODOLOGY
The problem selection process for different splits in miniCTX follows three main criteria: (1) ensuring new problems are less likely to have appeared in training data, (2) utilizing an automated selection process, and (3) promoting generalization. Depending on the properties and goals of each split, we adopted three primary approaches:
1. Recency-based selection: For popular libraries such as Mathlib and SeiLean, which are highly likely to be used for training, we aim to select newly added theorems. This achieved by sorting theorems based on the timestamp of when the theorem was first added to the project, which is extracted by NTP-TOOLKIT. This helps mitigate data contamination.
2. Random selection:
For more recent projects, such as the PFR split, where the risk of data contamination is lower, we randomly select proved theorems ensure representative sample of the entire project. This approach maintains generality of the selected problems.
3. Dependency-base baased selection: To explicitly evaluate models' performance in context- dependent proving, we selected files based on the in-file and cross-file premise labels available in our benchmark. For the PNT split, we chose the file with the highest number in-file dependencies. while for PFRerosflle we selected files with the highest cross-file dependencies. For HEP, we selected files with balance of both types. The level of dependency is also extracted automatically by NTP-TOOLKIT.
Although human inspection and expertise are involved in ensuring that the selected problems are valid and sufficiently general for evaluating models across diverse settings, all selection processes are ultimately automated by using the labels extracted through our toolkit. This ensures consistency across the benchmark and scalability to future updates.
3.3 KEY FEATURES AND CHALLENGES
miniCTX introduces several key features that distinguish from other theorem proving benchmarks, addressing challenges that have not been tackled by previous benchmarks:
Real-world theorem proving. Unlike popular benchmarks (e.g., miniF2F (Zheng et al. 2022), ProofNet (Azerbayev et al., 2023), FIMO (Liu al.) (023) that focus isolated competition problems, real-world research-level theorem proving is heavily dependent on rich mathematical contexts. Therefore, mini CTX includes real-world, complex theorems from a variety of ongoing Lean projects, such as Prime Number Theorem (PNT) and Polynomial Freiman -uzsa Conjecture (PFR). They rigorously test model's 's ability in real-world formalization projects. This diversity contrasts with the LeanDojo benchmark (Yang et al.) (202)), which focuses solely on Mathlib, enabling miniCTX to better test model's generalization in different settings.
Contextual evaluation. Proving a theorem often depends on new definitions, lemmas, other contextual information, which model may not have seen during training. miniCTX includes theorems along with this new context. During evaluation, the model is expected to leverage the provided new context to help prove the theorem.
Beyond previous datasets like LeanDojo (Yang et al. 2023) and CoqGym (Yang & Deng 2019), which include relevant definitions and theorems, miniCTX includes additional useful contextual information that may make some theorems easier to prove compared to standalone theorems. For instance, Lean source code can have natural language comments that may help constrain the space of possible proofs. Moreover, some proofs within file often have analogous patterns or structure, which
5

---

Published as a conference paper at ICLR 2025
may make subsequent theorems easier to prove (see $A.2). These additional forms of context occur in the real-world process of formalization, yet their use in neural theorem proving is underexplored.
Automatically updating the benchmark. Most modern neural theorem provers use large language model as a backbone. Therefore, it is crucial to ensure that evaluation content is not scen during pre--ttrinning problem not addressed by previous benchmarks (see ŞG). We plan update mini CTX
periodically to include theorems beyond a certain cut-off date (see our project page). Future updates
will be automatically extracted from new Lean projects using NTP-TOOLKIT ($3.4). See Feeeue 2
GPT-4o, DeepSeek training cutoff
Future LLMe training cutof
File cirtert
2023
2024
2025
Agr Agliliinn leanty
Lear Raurmm
Now our Bocaaa
Preop Stawe Prose
prive
Prool to
minsCTX compiled new Lean theorems
MiniCTX-v3 compiled newer Lean theorems Evalusto using future LLMs
Previous benchmarks compiled with Lean theorems (Mathlib, miniF2F)
Presf StaTe from Lawn
Mort Ctactic )
Evaluate using GPT-4a, Deep
Next Ktop
C'occtic )
miniCTX is automatically updated with Lean projects to stay ahead of LLM training cutoff dates, making a suitable benchmark for real-world theorem proving for pre-trained models.
Figure 2:
Stater Tiningg
File Turing
Figure 3: State-tactic vs. file tuning.
3.4 NTP-TOOLKIT: AUTOMATED DATA EXTRACTION AND EVALUATION
We provide TOO-KOO that automatically extracts mini CTX and metadata. NTP-TOOLKIT also used to extract data for training baselines, and it provides an interactive Lean evaluation environment.
Data extraction. NTP-TOOLKTT contains a general- purpose data extraction tool that extracts examples from arbitrary Lean 4 repository and formats them into individual theorems in miniCTX. The tool is implemented in Lean based on lean- ttraninnnddaae data (Morrison) (023). Specifically, NTP- TOOLKIT takes in configuration file with some Lean repositories specified. Then for each theorem in each repository, it outputs a SSON-formatte entry in miniCTX, including the full context information, theorem statement, and proof. It also extracts useful metadata that used for automated problem selection in miniCTX (see $3.2). and for our experimental analysis. See Appendix A and C for the formats provided by the data extraction.
Interaction via Lean REPL. In order to evaluate model on miniCTX, a model needs to efficiently communicate generated proofs with Lean and receive current state and error information. To better integrate LLMs and Lean, we developed a Python wrapper for the Lean Read-Eval-Print Loop (REPL) (Lean Prover Community 2024). The Lean REPL offers an interactive environment for submitting code to and receiving messages from a Lean instance. We provide a Python interface for (1) submitting both complete Lean proofs and individual tactics, and (2) receiving and handling feedback from Lean, such as error messages indicators that tactic application is valid or a proof is complete. This interface enables simpler evaluation on the miniCTX benchmark.
4 EXPERIMENTS
We evaluate several baselines on miniCTX, demonstrating the importance of context in real-world theorem proving. We study performance along various axes, including premise dependency, context length, difficulty, and the type of information the context. Our experiments show that file-tuned models, which can utilize context at evaluation time, improve drastically over traditional state-tactic models in the context dependent setting. Moreover, we discover that this real-world performance boost cannot be readily measured by existing benchmarks such as miniF2F. Our investigation reveals several open challenges that we discuss in $
Training data. We ran NTP-TOOLKIT'S next-tactic extraction on a 2023 snapshot of Mathlib, yielding 709 examples. We then ran VOP-TOOLKITY instruction tuning script on these examples, yielding training examples and for stte-taccic and file-tuning (see I4.1). For the file-tuning examples, as an initial method for handling the long Lean files, we either truncate the middle of an input file so that the file contents is 1024 tokens, or take only the preceding 1024 tokens, with the strategy selected

---

Published as a conference paper at ICLR 2025
random for each example. We open-source our training data for both file-tuning and tactec tuning, split into 583k train, 15k dev, and 15k test examples.
4.1 BASELINES
We select several baselines that evaluate on miniCTX, as follows:
Prompting LLMs. We first test the ability of state-of-the-art API-based model, GPT-4o, to generate the complete proof given theorem statement in Lean, with several few-shot examples provided for guidance. We generate 8 such proof samples and measure pass @8 proof rate. We also test whether adding context the form of preceding file contents or retrieved premises improves the proof rate.
State-tactic prompting, Another common approach to theorem proving using language models is the model generate tactic given the current proof state (Han al., 2022, Yang et al. 2023 Polu & Sutskever, [020] Lample et al. (022).. Therefore, we test the factic prompting setting, which prompts a model specialized for mathematical tasks, Llemma-75 (Azerbayev et al., 2024). to output a tactic given proof state. At test time, the model generates one tactic at time, and we use best-first search construct full proofs (Han et al. 2022 Yang al. 2023 Polu & Sutskever 2020).
State-tactic tuning. We can further improve tactic generation by fine-tuning language models on human-written (state Zt, tactic I/b pairs. We follow this state-tactic framework and fine-tune state-tactic tuned model from Saapseee--Codr--.333 (Guo et al. 2024) to input proof states and output tactics, trained on muman-written tactics in Mathlib, the main mathematical library in Lean, extracted TTO-KOOLII Similarly, use best-first search at test time.
File-tuning. drawback to the setups above that they only consider static (state, tactic) pairs, and do not take into account context, including comments, definitions, lemmas, and file structure, encountered during test time. Therefore, we test whether supplying context C, in the form of preceding file contents, the model improves performance. Similar state-tactic tuning, tune SeaSeeek-Code--... on human-written (state Zt, context tactic yt) triples to generate tactics based on the current context and proof state, resulting the file-tuned model (see Fiiuree 3).
fine-
Premise selection. While in-file context offers valuable information to models, it still overlooks external resources like imported modules, which are often crucial in real-world interactive theorem proving. To better simulate a complete context and evaluate on project-level generalization, we apply premise selection to extract relevant premises from imported files within the same repository. Specifically, we use the premise retriever provided by LeanDojo (Yang et al. (023) to identify the
top 20 most relevant definitions or lemmas from imported modules and append them to the in-file context. Given that the models we are evaluating are trained on Mathlib, and they exhibit strong ability to apply Mathlib lemmas, we did not include Mathlib in the potential premises to ensure that the models gain much information possible from the provided context (both infile and crossfile). All potential premises are automatically extracted using our toolkit, ensuring an efficient and automated process.
Table 3; Performance comparison (%) of different models miniF2F-test and mini CTX-tst.....
miniF2F
MiniCTX-test
Method
Test
Prime
PFR
PFR
Mathlib
HTPI
HEP
SciL.ean
Avg.
GPT-4o (full proof)
13.52
7.06
1.85
6.98
14.00
13.33
31.15
6.52
11.72
context
31.76
5.56
34.88
26.00
17.78
49.18
17.39
27.08
context premise
29.41
7.41
39.53
15.56
44.26
21.74
26.82
State-tactic prompting
28.28
20.00
5.56
0.00
16.00
0.00
31.15
19.57
14.58
State-tactic tuning
32.79
17.65
5.56
0.00
22.00
11.11
52.46
19.57
19.53
File uniig
33.61
40.00
5.56
44.19
34,00
15.56
60.66
45.65
35.94
premise
42.35
11.11
16.28
8.89
50.82
32.61
30.21
4.2 RESULTS
Context-dependent methods improve theorem proving, Table 3 shows baseline performances on miniCTX. We see a dramatic improvement for the file-tuned model (trained on full file context) over the state-tactic model (trained only on proof states) (35.94% vs. 19.53%). Similarly, providing
7

---

Published as a conference paper at ICLR 2025
Performance on thearems by in file dependency
Perfarmance e en miniCTX thearems by dependency level
State ta ctic tuning File-tuning
GP1-40
Performance (%6]
0.6
0.6
GPT-4
0.5
0.5
GPT-4o + context premise
0.4
Performance
0.4
0.3
0.3
0.2
0.1
0.0
0.0
With dependency (miniCIX)
Low dependency all premises
High dependency High dependency High dependency in-file premises cross-fle boos-fill premises premises
problems (miniF2F)
dependency (miniCTX)
Figure 4: Model performance by dependency on premises. For each theorem in miniCTX, we record as metadata whether its human-written proof depends other definitions theorems in the same file ("in-file") or other files ("cross-file") and test the performance baselines on each type.
the preceding file context, which includes definitions and lemmas, to GPT-4o results in dramatic improvement compared to using just proof state (27.08% vs. 11.72%). These findings highlight the importance of providing models with rich contextual information beyond the immediate proof state, also demonstrating that miniCTX able to measure this ability of context-dependent proving.
Premise selection improves performance on high cross-file dependency splits. The results in Table indicaae that premise selection has a mixed impact on model performance. For the GPT-4o, premise selection improves performance
high cross- file dependency splits, such as PFR, PFR and SciLLean This suggests that premise selection helps capture the cross-file context, enabling GPT-4o to make better use of cross-file information. However, for the file-tuned model, premise selection does not consistently improve results, and even performs worse on the PFR split, which was designed evaluate the effective premises differ significantly from the in-file context. Therefore, developing methods that effectively support the integration of cross-file context (e.g., premise selection) alongside in-file context remains an interesting open research direction for improving performance on the miniCTX benchmark.
of cross-file premises. This suggests that the retrieved
Evaluation on miniF2F. We evaluate baselines on miniF2F, a standard benchmark based on compe- tition problems that do not require context. We use import statements as context for the fileetuned model. The file-tuned model improves very little beyond the state-tactic model (33.61% 11 vs. 32.79% showing that the dramatic difference in context-dependent proving abilities seen on mini CTX cannot be captured by miniF2F.
4.3 ANALYSIS
We analyze the baseline models on miniCTX further along several axes, including the kinds of contextual dependencies, the difficulty, and the content made available in the context.
File-tuning especially helps on problems with infile dependencies. We use the mini CTX metadata categorize theorems based on their in-file dependencies. FFigure 6 shows the performance of state-tactic tuned model and file-tuned model on problems with in-file dependencies compared to those without. We also show miniF2F an additional reference point for problems without in-file dependencies. The file-tuned model shows marked improvement over the state-tactic tuned model, especially in problems that have dependencies on context. We conclude that file-tuning specifically helps in the realistic setting of theorem proving with new definitions and theorems in context.
Premise selection helps but may interfere with in-file context. We use mini CTX metadata to categorize problems based on their cross-file dependencies, evaluating the impact of premise selection across the entire dataset. As shown in Figure 4| GPT-4o benefits significantly from premise selection on problems with high cross-file file dependencies, showing improved performance when leveraging relevant premises from imported files. However, we also observe that premise selection can interfere with in-file context, leading to inconsistent results, particularly when the available in-file context is relatively short. This suggests that adding cross-file premises may sometimes disrupt the model's ability to focus the in-file information. Further analysis of this interference is included in $D.3 This highlights the need for more sophisticated integration strategies that can balance both in-file and cross-file contexts effectively.
8

---

Published as a conference paper at ICLR 2025
Table 4: Ablation study on different context components for theorem proving.
Enviromment
Definitions
Lemma Statement
Lemma
Natural Language Comments
File-tuning
GPT-4o
Proof
X
14.12%
8.24%
25.88%
2.35%
/
24.71%
9.41%
/
27.06%
22.35%
/
32.94%
34.12%
28. 28.24%
23.53%
35.29%
31.76%
Models learn from previous proofs in the file context. To determine the contribu- tion of different components in the in-file context, we conducted an ablation study on the AFR.ForMathli. Entropy. Basic file, which contains numerous co-related lemmas and rich natu- ral language comments, making it an ideal candidate to investigate the influence of different context components. In this ablation, systematically removed specific parts of the in-file context and evaluated the model's ability to generate proof's under these modified conditions. As shown in Table 4] both the file-tuned model and GPT-4o benefit from the inclusion of previous proof's in the file context. This indicates that models are capable of learning proof strategies from existing proofs in the file and effectively applying them new problems (see $D. for more examples).
Natural language comments contribute in certain settings. Our ablation also explored the effect of natural language comments in the in-file context. Though the impact was not dramatic, comments written in natural language were found to be helpful in certain settings. In scenarios where proofs were excluded from the context, adding comments resulted slight performance gains for both models. For the file-tuned model, these gains were further amplified when proof' were included alongside comments, demonstrating the value of combining formal context with explanatory natural language. However, for GPT-4o, the presence of comments when proofs were included led to slight decrease in performance, suggesting that effective context selection may vary depending on the model architecture and underlying training characteristics.
File-tuning improves across all difficulty levels and context lengths. Finally, Appendix DD2 shows performance problems categorized by the length of the human-written proof (when available), which we take as a rough proxy of the problem difficulty. The file-tuned model improved on all three difficulty categories. Appendix |D22 shows that file-tuning had improved accuracy context lengths, particularly for problems with longer contexts. Longer contexts may imply more dependencies, suggesting that these problems can benefit more from file-tuning.
Models rely on common symbolic automation. To demonstrate an additional kind of context- dependence, we perform an additional analysis on Math2001 (Macbeth 2023). which is another Lean textbook setting 2 In particular, the textbook code disables powerful automation tactics including simp and linarith promote manual reasoning, akin to traditional textbook exercises. For example, Math2001 includes numerous arithmetic problems that are trivial with automation tactics (e.g., linarith) but are challenging for models to explicitly prove with step-by-step reasoning (e.g., via calc). In Table we evaluate models with the automation disabled, and observe substantial performance drops, confirming the reliance on automation tactics. We also find that the state-tactic tuned model relies simp for unseen definitions, making it performing similarly well to the file-tuned model on theorems that only rely on new definitions ($D.6).
5 DISCUSSION AND FUTURE CHALLENGES
In addition to general improvements in performance, comment some specific open challenges.
Making better use long-contexts. Our file-tuning method simply truncates contexts to be within token budget (1024), which can discard useful contextual information. We found gains in providing GPT-4o 8,000 tokens of context compared to not providing it context, but its absolute performance was still low. There several possible strategies that can be explored in future work, including feeding in the entire context, retrieval, or mixtures of the two.
"Se Appendix B.1 for further details on Math2001. Due licensing we do not include in miniCTX.

---

Published as a conference paper at ICLR 2025
Repository-level context. We focused evaluating in-file context in this paper. As shown in SD.I many problems require using context outside of the current file. Although we incorporated premise selection means of leveraging cross-file context, our experiments indicate that it does not consistently improve performance, even on datasets with high cross-file dependencies. This suggests need to further investigate how to better integrate premise selection with in-file context. miniCTX provides sufficient metadata to reconstruct the entire environment, allowing for comprehensive investigation into premise selection and other potential methods for leveraging cross-file context.
Challenging proofs. Using context through file tuning did not improve performance on the challeng- ing PFR proofs. Moreover, performance is relatively low (19%) on proofs that had a human- -writtnn proof of longer than five lines (see .D.)) Proving these kinds of theorems remains an open problem.
Working with constraints. As shown in Table 6 model performance drops when the proof cannot use powerful automation tactics. Models have tendency to invoke these powerful tactics, and struggle with more explicit step-by-step proofs. Improving performance this setting of miniCTX is an interesting future direction.
6 RELATED WORK
Formal theorem proving with language models. GPT-f (Polu & Sutskever, 2020)
pioneered the
use of language models for theorem proving via next tactic prediction given the current proof state, a
technique adopted by many subsequent methods (Jiang et al. 202T Han et al. 2022 Lample et al.
2022
Polu et al. 2022 Welleck & Saha 2023 Azerbayev et al. 2024 ReProver Yang et al.
2023) conditions each generation on retrieved premises, while Drait-sketch-pree
(Jiang et al. (2023)
conditions each generation on an informal proof. Baldur (First et al. (023)) fine-tunes model with 50 lines of the preceding file content as context, but unlike file-tuning trains the model to generate a full proof without proof states. More broadly, machine learning for formal theorem proving is an
active research area; see Lu et al. 2023 Li et al. (2024) for surveys.
Theorem proving data extraction. Several tools extract training data from interactive theorem provers, including CoqGym (Yang & Deng 2019) for Coq, PISA (Jiang et al., 2021) for Isabelle, LeanStep (Han al. 2022) for Lean 3, and LeanDojo (Yang al. 2023) for Lean 3 and 4. Recently, lean-training data (Morrison 2023) provides tools for extracting proof states and other infor- mation using Lean 4 metaprogramming. which anecdotally found to be easiest to modify and fastest among Lean 4 data extraction tools. Our NTP-TOOLKI adds 3 new tools on top of this code, along with a pipeline for running on any Lean projects and instruction tuning.
Theorem proving benchmarks. Theorem proving methods are typically evaluated in two settings: (1) standalone competition problems (Zheng al.
2022) textbook (Azerbayev et al. 2023) problems; (2) holding out theorems from a mathematical library that the model is trained on, such as Mathlib for Lean (Han al.
2022 Polu et al.) 2022; Yang et al.) (202)) or the Archive of Formal Proofs for
Isabelle (Jiagg et al. 2021 First et al. (023)) ).. The first does not test the use of context, while the
second tests only theorem-level generalization miniCTX is designed to test the use of context as well as theorem-level, context-level, and project-level generalization across several mathematical domains.
Premise selection. Premise selection is an extensively studied class of methods for handling context in theorem proving. These methods retrieve useful lemmas from previously proved results, to help prove the current theorem. Many recent premise retrievers embed theorems and premises to a common space, and then taking similarity measure (Yang al. 2023 Mikula et al.) 2023), or use classifier to determine if a premise is relevant (Irving et al. 2016 Han et al. 2022). Graph2Tac (Blaauwbrock) et al. 2024) proposes an online learning method that can learn from both proofs and premises in new context, which is particularly relevant to our work since it tackles project-level generalization. However, such methods cannot combine with more advanced pre-training-bart -based methods without risking data contamination during evaluation. miniCTX aims to fill this gap by our temporal split.
7 CONCLUSION
We studied the realistic setting of proving theorems that depend on new information and project constraints, and formulated an evaluation framework for testing generalization using real Lean projects. We built miniCTX, and found that the predominant method for training neural theorem provers fails to enable context dependent proving. Our file tuning method provides a strong starting point for the new challenges opened by our investigation into theorem proving with context.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGEMENTS
Sean Welleck thanks Convergent Research, the Lean FRO, and the OpenAl Researcher Access Program for their support.
REFERENCES
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards mathematics formalisation assistant using large language models. arXiv preprint 4rX15:2211.07524, 2022.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate--lvel mathematics. arXiv preprint arXiv:2302.12433, 2023.
Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen Marcus McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. In The Twelfth International Conference on Learning Representations, 2024.
URL
Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts, 2024. URL 2401.029999
https: http:s://axxiv..oo www.v.orgg/.....................
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole- proff generation and repair with large language models, 2023.
Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. Deepseek-coder: When the large language model meets programming the rise of code intelligence, 2024.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co- training for theorem proving with language models. In International Conference Learning Representations, 2022. httt:tttt//:/eeeeee
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016.
Albert Qiaochu Jiang, Wenda Li, Jesse Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. hotp::///aatpp-oofeeeeeee .rgeeeerrrg//// 2021 abtpaaattttttttrrraaaaaaa 17. pdf 2021.
Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdž, Piotr Mitoš, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. Advances in Neural Information Processing Systems, 35: 8360-8373, 2022.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference Learning Representations, 2023. URL httpp:://ooeneeeeer...o httpp//awrrii.eeee/e/ooooood/ttr
Alex Kontorovich. Prime number theorem and. TriieeNumberTheoreeee 2024a.
http:://ggtaab.cco//eleexotoooto
Alex Kontorovich. Prime number theorem and; rectangle.lean.
https://github.co com/
Rectangle lean, 2024b.
Guillaume Lample, Timothee Lacroix. Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337-26349 2022.
11

---

Published as a conference paper at ICLR 2025
2024. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, 2024.
Lean Prover Community. htgpl//tws.ggggtouo.ooo////eepee
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving, arXiv preprint urXiv22309004999 2023,
Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning, In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 6l Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. 14605-14631, Toronto, Canada, July 2023. Association for Computational Linguistics. doi: 10.18653/v1/0233.al acl.ooo.....-1..1........ URL htt.a/gsssaacaaaaoooggg.ooo/////
acl-long. 817
Heather Macbeth. The mechanics of httpss//ggghuo....o/mmrr.cctttta 2023.
Mathlib Community. The Iean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL '20. ACM, January 2020. doi: 041144//37228533338222
URLpttp:: //dx: doi owwooro/.../.... 10. 1145/3372885 3373824
Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kuciński, Piotr Mitoš, and Yuhuai Wu. Magnushammer: A transformer- based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023.
Kim Morrison. coen-training--ee https::/gittuu..coo/ss/m///// 2023.
tertaan-trriinngg data
Leonardo de Moura and Sebastian Ullrich. The lean theorem prover and programming language. In Automated Deduction-CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022.
Tomáš Skřivan. Scientific computing in lean. http:s///ggghhub..cc///l/ooppppp
2021.
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for thcorem proving in Lean. arXiv preprint arXiv: Arxiv-2404. 12534, 2024.
Terence Tao. Pfr. http:////ggttuuu..mootrtererreee
2023.
Joseph Tooby-Smith. Heplean: Digitalising high energy physics. arXiv preprint arXiv:2405.08863 2024.
Daniel J. Velleman. How Prove It: Structured Approchh. Cambridge University Press, edition, 2019.
Sean Welleck. Llmlean. https://githuu: com/ hmmpcmmmmm1/maa 2024.
Sean Welleck and Rahul Saha. Llmstep: Lim proofstep suggestions in lean. arXiv preprint arXiv:2310. 18457, 2023.
Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang. Zhibin Gou, Z. Wu, Fuli Luo, and Chong Ruan. propseek--oove--l1... Hamnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint 08 2024. URL
https://arxiv.. org wtwgab/////....... 08152
Kaiyu Yang and Jia Deng. Leamning to prove theorems via interacting with proof assistants, 2019.
12

---

Published as a conference paper at ICLR 2025
Kaiyu Yang. Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieeel-augmmenee language models. In Neural Information Processing Systems (NeurIPS), 2023.
Huaiyuan Ying, Shuo Zhang. Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. Intermlmmmath: Open math large language models toward verifiable reasoning, arXiv preprint arXiv:240.00333,, 2024.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: cross-system benchmark for formal olympiad-level mathematics. In International Conference Learning Representations, 2022. URL //operrevierr net/forrurriiesPPggffPPPy
13

---

Published as a conference paper at ICLR 2025
Appendix
A MINICTX EXAMPLES
Here give some examples of the miniCTX and its sources to illustrate the format of the data and how and why we collect certain theorems.
A.1 EXAMPLE ENTRY
An entry in the miniCTX dataset consists of the theorem statement, preceding file contents, and metadata information. For example, given the following theorem s_eq_pow_ in context:
import Mathlib. Data. Real. Basic
/-!
Square function
We define the squaring function "s R.R
R to be
-/
def s (x R) : R
lemma s_eq_pow_twe fx RD [a, pow_two]
-x=x- 2 :=
14

---

Published as a conference paper at ICLR 2025
We collect its data into miniCTX, formatted in JSON follows:
# Preceding file content
"srcContext"; "import_Machlib Data. Real.
htt.a//aaaaaaaaaaaaa/aaaataaaaae lnkey
htt.ieettteeuuuringgnuuuuu htgp ytouuu uU VVnn/ Aln)
utoubeu
# Theorem statement "cheoremStatement""
# Fully qualified theorem name "cheoremName": "e_eq_poR_two
# Temporal metadata
"fileCreated"; " "ggit__ommiit",,
"cheoremCreated": "(git_commit)",
# Source metadata
"file": MMpProject/Square.een lean "module": "MyProject. Squarre" "positionMetadata".
Line number the theorem is on "LineInFile": 10,
# Number of tokens before the theorem
" "ooteuPositionnnfilee 152,
Number of premises (definitions, theorems) before the theorem "cheoremPositiinnniilll!
},
# Dependency metadata
"dependencyMMetddtta"""
# Number of definitions or lemmas defined in this file that the theorem uses "'nPiiePremises": true, " "munInFiloPromisee""" 1,
Number of definitions lemmas defined in this repository that the theorem uses (including in-file ones)
"repositoryPremisee": true " humBepositorrPPremisss""" 1, Number of total premises (in file, repository, otherwise) "nunPremises": 2,
Modules imported in the current file "importedMouules" ["Mathlib. Real. Baal.Baic",, ...]
# Proof metadata "proofMetadata": { "hasProof": true,
"proof": "by::"yynnaaan www...........oo.ttooo "proofType"; "tactic", "proofLengthliines:: 2,
"prooflengthtokenes". 20
}
In additional to individual entries, we also record the version (git commit) of the repository.
A.2 PRIME NUMBER THEOREM EXAMPLE
We collect theorems from the Rectangle e lean file in PrieNuunbeTTheormmAdd The following excerpt from Rectangle. lean demonstrates scenario that often arises in theorem proving environment where context is critical to producing proof:
import Aathlib.nnalysti Complex. CauchyIntegral import Mathlib. Analysis Complex. Complex.Conee: Convex
15

---

Published as a conference paper at ICLR 2025
open Complex Topology
open scoped Interval
variable (z C} fa R}
7-%%
(bogin(definition) ooge
Rectangle has corners $2$ and $w \in \CS.
kend(definition)
2%-/
/-- A Rectangle" has corners "z" and "w". -/ def Rectangle (z C) Set C := [[a.re, w.rel] xC [Iz.mm, w.im]]
namespace Rectangle
lemma symm : Rectangle z Rectangle by simp [Rectangle, uIcc_comm]
lemma symm_re Rectangle (v.re 2. z.im I) (z.re w.im simp [Rectangle, uIcc_comm]
Rectangle w by
When proving the final lemma symm_re, model can benefit much from the preceding file contents, which include (1) the existing imports from Mathlib, varia aable declarations, and open namespaces that provide syntactic context for this theorem, (2) the new definition Rectangle in the context, which the model has not seen training, (3) natural language and LaTeX documentation the file
and Re Rectangle definition, (4) the analogous (in this case identical) proof of the preceding theorem symm. We demonstrate that performance on Rectangle. lean is indeed much higher when preceding file contents are given context model.
For future data added to miniCTX that specifically test the preceding file contents as context, we will ensure it is standalone like Rectangle lean, i.e. it does not import any other unseen files from the same repository, so the preceding file contents already contain all important information relevant to the proof.
B ADDITIONAL DATASETS
In addition to problems in miniCTX, we also evaluated other datasets that are not included due to copyright reasons.
B.1 MATH2001
Math2001 (Macbeth 2023) contains the Lean code for the book The Mechanics of Proof by Heather Macbeth, introductory text mathematical theorem proving with accompanying Lean code. Each chapter The Mechanics of Proof covers an introductory topic and walks through how to write the associated mathematics in Lean, along with exercises. The topies include proofs by calculation, proofs with structure, parity and divisibility, logic, induction, number theory, functions, sets, and relations. A unique aspect of Math2001 is that disables common Lean automation for pedagogical purposes. For example, student must write out an equality proof in detail, with each step justified. also defines new tactics and definitions separate from the common Lean libraries. Typically file in the textbook will show examples of such proofs, followed by exercises for a student to complete. We can view this as form of contextual adaptation: model must prove the theorem according to the constraints of the textbook. Math2001 has 41 files that include examples and exercises. We selected theorems from each file (depending on the length of the file), for a total of 50 theorems. Of these, 31 have no proof in the Math2001 repository, hence testing theorem-level generalization.
Context-aware models surpass state- based models Table shows the performance comparison of different models. Both the GPT-40 model, which includes context in the input, and the file-tuned
16

---

Published as a conference paper at ICLR 2025
Models
Math2001
GPT-4o (full proof)
11.76%
GPT-4o context)
43.13%
State-tactic prompting
31.37%
State-tactic tuning
27.45%
File tuning
41.18%
Table Performance comparison of different models on Math2001.
Automation
File (%)
State-tactic (%)
Enabled
41.18
11.76
Disabled
27.45
7.84
Table Performance on the Math2001 split with and without access to standard automation.
model perform significantly better than the other models. This demonstrates the importance of context information in context-dependent textbook-style problems.
Models rely on common symbolic automation. The Math2001 split originally disables powerful automation tactics including simp and nlinarith to promote manual reasoning, akin to traditional textbook exercises. Table we evaluate models with the automation disabled, and observe substantial performance drops, confirming heavy reliance of current models these automation tactics. An examination the training corpus further revealed a general dependency on automated tactics within real Lean projects, indicating that models have learned to rely these tacties.
C NTP-TOOLKIT AND FILE-TUNING DETAILS
C.I DATA EXTRACTION
VTP-TOOLKTI contains general-purpose data extraction tool that extracts examples from an arbitrary Lean 4 repository and formats them into examples that be used compile miniCTX, well as for language-model fine-tuning. The tool is implemented in Lean based on Kim Morrison's s lean-training-data.
Specifically, NTP-TOOLKIT takes in configuration file with one or more Lean repositories specified. Each repository is transformed into next-tee extt-tacti and full proof examples stored in JSON Lines files. The next-tactic data is suitable for making file-tuning examples of the form (context, state, next-tactic):
"state": tactic state
"nextTactic"; # pretty-printed next tactic, "arcUpToTactic": # source code in the file up to the tactic invocation, "decl": # declaration without proof (e.g., statement of theorem), "declUpToTactic" source code in the declaration up to the tactic invocation, "declId"; unique identifier of the declaration
The full proof data is suitable for making evaluation examples of the form (context, theorem, proof):
"srcUpToDecl"; source code in the file up the declaration, "decl": # declaration without proof (e.g., statement of a theorem), "declId"; # unique identifier of the declaration, "proof": proof
Full proof data is also suitable for training model to directly generate a full proof, and NOP-TOOLKIT also provides Lean source with proof states interleaved, both of which do not explore in this work.
17

---

Published as a conference paper at ICLR 2025
C.2 INPUT-OUTPUT FORMATTING.
Below we show the imputs and outputs for file-tuning and state-tactic tuning. In the paper refer to the natural language description at the beginning of the input as an "instruction", and refer to a set of inputs and outputs as described below as "instruction-uure -tuning data".
C.2.1
FILE TUNING.
Given an example containing state, next-tactic, and preceding file contents (arcUpToTactic), the data is formatted
Input:
/- You are proving theorem Lean
You are given the following information:
The file contents up to the current tactic, inside [CTX] ... [/CTX] The current proof state, inside [STATE] [/STATE]
Your task is to generate the next tactic in the proof. Put the next tactic inside [TAC] [/TAC]
-/
[CTX]
(srcUpPoTactic)
[/CTX]
[STATE]
(state}
[/STATE]
[TAC]
Output:
(nextTactic}
[/TAC]
C.2.2 STATE-TACTIC TUNING.
Given example containing state and next-tactic, the data is formatted
Input:
/- You are proving theorem in Lean You are given the following information:
The current proof state, inside [STATE] ... [/STATE]
Your task is to generate the next tactic the proof. Put the next tactic inside [TAC] [/TAC]
-/
[STATE]
(state)
[/STATE]
[TAC]
Output:
18

---

Published as a conference paper at ICLR 2025
(nextTactic) [/TAC]
C.2.3 GPT-40 PROMPT
For full proof generation task with only theorem statement, the following prompt:
Your task is to generate complete proofs for problems stated in Lean4. You may use any tactics available in Mathlib, but no additional context, definitions, or theorems from the problem's 's file will be provided. Focus crafting proofs using general knowledge and techniques applicable in Lean4. Here are some examples:
1 1emma deriv_scale {f CS (n 1) (f.scale R) .erivv R
f. s.deriv.scale R :- by ext v by_cases hR
<;> simp [hR, scale]
simp [deriv, smul] exact deriv_ const
exact ((f. hasDerivvt (R-1 v)) .ccomp v (by simpa using (hasDerivAt_id
v) const_smul R R)
mul_dvd_mul_lett theorem mul mul_dvd.__ mmm_mlleee left (a a) (h : a obtain (d, rfl) := h
Iw [mul_assoc]
/- Now here is your exercise. There is no need to restate the problem. If needed, think through the proof using comments. -/
(theorem statement)
19

---

Published as a conference paper at ICLR 2025
For full proof generation task with additional infile context, the following prompt:
Your task is generate complete proofs for problems stated in Lean4. For each problem, you will be provided with the context from the file in which the theorem is stated. This context includes useful external libraries, along with important definitions and theorems that are relevant to the proof. You are encouraged to use any tacties, definitions, lemmas, or theorems defined within this context to construct your proof. Please pay careful attention to indentation and formatting to ensure that the proof adheres to Lean4 syntax standards. Here are some examples:
#Context:
import Mathlib. wwt.iii..aallsii...mmmm Calculus Seriv.Support import Mathlib Mathlib.Anaalsiis import Sethlib.Ordes Filteer ZeroohndBouuddddtFiileee
SchwartzSpace
open Real Complex MeasureTheory Filter Topology BondeeCoorinmoouuPPuctcioo SchwartzMap BigOperators
variable {E Type*} [NormedAddCComGrruu E]
[NormedSpace IR
E]
{(n
N}}
[[ext] structure CS (n N) Type*) [NormeddcdCCommrroup [NomedSpacce
R E] where
toFun R -
h1 ContDiff R toFun
h2
HasCompactSupport toFun
noncomputable def scale (g CS n E) (R by_cases h =
RR)
CS n E : by
exact (0, contDiff_conse funscale g x, ?_ ?_)
simp [HasCompactSupportt, tsupport])
refine (fun
exact g comp (contDiff, coattDif_ccont..... contDiff_id)
exact g h2. comp_smul (inv_ne_zexs h)
/- Truncated -/
/- Now here is your exercise. There is no need to restate the problem. If needed, think through the proof using comments. -/
#Context:
0
#Problem:
O
(theorem statement)
20

---

Published as a conference paper at ICLR 2025
D ADDITIONAL RESULTS AND ANALYSIS
We present additional analysis on the composition of miniCTX and additional quantitative and qualitative evaluation of performance on miniCTX. All tests in this section are done on miniCTX-tes
D.1 DEPENDENCY DISTRIBUTION
Praportion of different dependencies
Percentage of theorems (96
100
Depends Iniflie difinitions
Depends In-tile thearems
Depends on In-repo. derinitioss
Depends on In-repo, theorems
Figure 5: Percentage of different dependencies in the human human-written proof of theorems mini CTX.
D.2 PERFORMANCE BY PROOF LENGTH AND CONTEXT LENGTH
Performance on theorems by dependency type
State-tactic tuning
File-tuning
40
Performance (%)
30
20
10
0
Standalone No in-file problems (miniF2F) dependency
Definition dependency
Theorem dependency
All dependencies
Figure 6: Performance by dependency type. For each theorem in miniCTX, we record metadata whether its human-written proof depends on other definitions or theorems in the same file, and test the performance of baselines on each type. File-tuned models substantially outperform state-tactic tuned models on theorems with definition and/or theorem dependencies.
D.3 INTERFERENCE BETWEEN IN-FILE CONTEXT AND RETRIEVED PREMISES
our experiments, we attempted to supply both in-file context (in the form of preceding code) and premise context (in the form of retrieved premises) to GPT-4o for proving theorem. In |igure present an analysis of the impact the length of retrieved premises on the resulting proof success rate.
Longer retrieved premises hurt performance. The results indicate that problems with lower premise-tor coalsee-t-coontee to-context length ratio tend to have higher success rates. Specifically, successful problems often feature relatively shorter premises proportion of the full context length. This suggests that models are better able to utilize and focus on relevant in-file context when the cross- file premises proportionally smaller. Conversely, when the length of the premises becomes relatively large
21

---

Published as a conference paper at ICLR 2025
Performance by proof length
Performance by in-tile context length
State tactic tuning File-tuning
State tactic tuning
File-tuning
60
Performance
Performance
40
40
20
2-5
3000-8000
8000
Proof length (lines)
In file context (tokens)
Figure 7: Performance of two baselines on different difficulty levels and context lengths, as measured by the length of human-written proof lines and the size the preceding file contents tokens. File-tuning substantially improves theorem-proving abilities across all cases, but especially when the theorem is casier and the context longer.
compared the full context, it may overwhelm or distract the model, reducing ability to effec- tively utilize the in-file information. This finding highlights the importance of ensuring balanced integration of premises with the in-file context to maintain model focus and improve proof generation performance.
Performance by size retrieved premises
Success
Failure
0.0
0.1
0.2
0.3
0.4
0.5
0.6
0.7
0.8
Total size of retrieved premises, proportion of prompt
Figure 8: Impact of length of retrieved premises GPT-4o model performance. A higher premise- to-context length ratio correlated with lower success rates, suggesting that too much premise in context overwhelms the model.
D.4 EXAMPLE OF LEARNING PROOFS FROM CONTEXT
The file-tuned model is able utilize the proofs in the context. Here an example of the model making minimal modification to the proofs from the context:
Inpul:
theorem Set.lefte coot__mem_Ioo {a b R} & Set.uIoo b := fun (h1, h2) left_lt_aupp mp h2) [ee_o__no__l_ (inf fiff_lt_lee lt_left..p h1))
theorem Set bet.rright_not_mmm_u (a b R} : b & Set.uloo := by
Output:
22

---

Published as a conference paper at ICLR 2025
rintro (h1, h2)
exact (right_lt__an mpp h2) _e_of_not__a (inf Sinf__t_righttti mp h1))
D.5 EXAMPLE OF USING THEOREMS FROM CONTEXT
The file-tuned model able to utilize the stated theorems in the context. Here is an example of the model using the previously defined theorem in the proof:
Input:
1emma RectSubRect {Xu X1 X2
Xa yo Y1 Y2 Ya R) (Xo (xo_le_Xi X S x1) S x3) (yo_le_yi
(11_e__1
x1 S x2)
(x2_le_xg
yo S yı) (y Ve__le_y2 S y2) (y2_le_ys
y2 ys)
Rectangle (x1 Y1 (x. y2 C Rectangle (xo yo (xs y3
1) : by
Iw Lffet_subset_iff, mec_Rect, Rec_ refine ((?.. ?_ ?_, ?_), ?., ?., ?_, ?_) all all_goals simpa using by linarith
1 enma RectSubRect {2o
22 23
C} (xo_le_Xx zo.re S 21.re) (xI (xi_le_X2
2i.re I ze.re)
(x;_le_Xg Z2.re zg.re) (yo_ -e_lle_y: zo.im zi.im) (yi_le_y2 21 S im.im)
(y2_le_ys 22.im 23 2g.1m)
Rectangle 21 C Rectangle 2o 23 :- by
Output:
simpa using RectSubRect xe_le_xi xi_le_xa xe_le_xs yo_le_y y1_le_y2 le_ys
D.6 EXAMPLE OF USING UNSEEN DEFINITIONS
The trate-tcctic tuned model able to utilize the unseen definitions that appear the proof state. In the following example Set. uIoo is newly defined definition, which is never seen for state-tactic tuned model:
Input:
23

---

Published as a conference paper at ICLR 2025
theorem uIoo_ of le fa Type*} [Lattice al {a b of (h S b) Set. uIoo Ioo a b == by
[STATE] goal
zw:
c: R
a: Type u_1
inst: Lattice
ab:
h: a a
uIoo a b Ioo [/STATE]
Outpul:
simp [uIoo, h]
This leads the state state-tactic tuned model to perform similarly well as the file-tuned model on problems that only rely on new definitions, and not new theorems (see Figure 6
E DATASET HOSTING AND MAINTENANCE
MinicTX is released on HuggingFace: 13lab/ mimimiiiiiiimmmmii CTCXX distributed under the Apache 2.0 license. Data extraction tool TOO-KOOLKIT is released on GitHub: cmu-13/ntp-toolkit under the MIT license. We note that the underlying data for the individual splits of miniCTX are also released under the Apache 2.0 license. We include the licensing information in the dataset repository. We plan regularly update and maintain the dataset include examples from projects. For information about future updates such as miniCTX-v2, please refer to our project page: hhtpss 7/ //cmu-13.2g w...ggithu..... io/minicts..
F NTP-TOOLKIT GUIDELINE
We introduced NTP-TOOLKIT in With the NOP-TOOLKIT, users extract and annotate new theorems and proofs from any valid Lean project, in miniCTX format. The extracted data can be used either updates miniCTX training data (for which also provide instruction tuning utilities). We also develop lightweight evaluation framework for easy evaluation on miniCTX.
F.1 PRELIMINARY
The evaluation code relies heavily on the Lean REPL (Lean Prover Community, 2024). which operates within the project environment. Therefore, it is essential that the project builds without any errors. Additionally, the version of Lean used in the project should match the version supported by the REPL. While the Lean REPL supports versions > 4.3.0, for the hest experience with data extraction and evaluation, we recommend evaluating projects that use Lean version 4.7.0 0 or higher (all miniCTi CTX theorems are in 4.7.0). We plan to continuously update NTP-TOOLKIT support newer versions.
F.2 USING THE NTP-TOOLKIT
The NTP-TOOLKIT is designed to easily extract and annotate theorem proving data from Lean projects, by simply providing the project URL. To use the NTP-TOOLKIT for data extraction, follow these steps:
24

---

Published as a conference paper at ICLR 2025
1. Installation: Clone the NTP-TOOLKIT repository from GitHub your local machine. Cur- rently, to use NTP-TOOLKIT for Lean version 4.7, switch to the lean-v4. 7.0 branch; for 4.8.0 above. use the main branch. Ensure that you have the required dependencies installed, as listed in the repository's 's README file.
2. Configuration: Supply GitHub URL,, commit hash, and root modules of your Lean project in a JSON configuration file. Make sure that your project is using compatible version of Lean. NTP-TOOLKIT will extract data from all modules imported by the root modules.
3. Data extraction: Run the data extraction script provided by the toolkit. Specify the --full_proof _tt_iittrtinnniiieeeeeeee data and --premisee ses options to extract mini data, which will be stored in an sonicttxjsoo option to additionally extract the premises in each module, for premise retrieval. The full_ full_proof._ ttriniinnndaaeeee data outputs can be additionally used for fine tuning (assuming the extracted data is dated before the current temporal split of miniCTX).
output file. Specify the --declarations
For detailed commands and additional options, please refer to the README file in the NTP-TOOLKIT repository.
F.3 MINICTX EVALUATION
We provide a comprehensive evaluation pipeline the mini repository, supporting both factic-rrediction and full-proof generation tasks. Users should place the extracted JSONI. file from the NTP-TOOLKIT into the data folder. To run an evaluation task, execute the task script by specifying the dataset path, the corresponding project path, and the path to the Lean REPL. This setup ensures that the evaluation is conducted within the correct environment and with the necessary data inputs.
G DATA CONTAMINATION IN EXISTING BENCHMARKS
One of the contributions of miniCTX is the temporal split: using NTP-TOOLKIT, miniCTX only includes theorems created after certain cut-off date. This ensures LLMs trained before this date have not seen problems in miniCTX. We claimed that existing benchmarks face significant risks of data contamination, and here we provide some evidence this claim.
With regards to contamination, existing benchmarks can be largely categorized as either extracted from standard mathematical library (e.g. Mathlib), curated competition-style problems. For the former category, evaluation benchmarks include Mathlib test problems extracted by LeanDojo (Yang et al. 2023) PACT (Han al. 2022). as well as datasets like CoqGym (Yang & Deng 2019) and PISA Viang et al. 2021) in other formal languages. They are inherently at risk of contamination, because they are statically sourced from projects on GitHub, many of which have existed for years (e.g. Mathlib has existed since 2017). On the other hand, virtually all modern language models are pre-trained on public GitHub code, and have therefore seen the proofs. This partially invalidates any evaluation results using these henchmarks.
On the other hand, we have empirically found many solutions of datasets like miniF2F (Zheng et al. 2022) online. The original repository of miniF2F already contains full solutions to 72 of the 244 test problems (in Lean 3, which is directly translatable to Lean 4 Moreover, of the remaining problems, 12 IMO problems have full solutions in Mathlit") and Compfiles (a catalog of Lean proofs of competition problems at the time of writing. In total, at least 84 of the 244 problems in miniF2F-test, including 12 of the 19 IMO problems, have full solutions on GitHub. This may be an inherent issue of small competition-style benchmarks, as the theorem-proving community itself has significant interest in formalizing competition problems and solutions. The scarcity of problems from competitions like IMO each year, as well as the bias to only formalizing some categories (gcometry problems are often not formalized due to difficulty) also contribute to this issue. Whether temporal split and other mitigation methods can be applied to competition-style benchmarks may also be an interesting future direction of research.
http::///gthab.bcc////eeaa/////p
http://gihhhh.ccaarrrraaa//ammpt
25


Reviews:
[{"review_id": "bHfIs5AN3M", "reviewer": "Reviewer_gDKA", "summary": "This paper introduces $\\texttt{miniCTX}$, a benchmark of 384 problems with context-rich information, e.g., in-file definitions and lemmas, and evaluates the model's theorem-proving ability under new context, which claims to be closer to the real-world scenario when researchers develop the formal repository. The paper further includes the NTP-TOOLKIT that the authors use for data extraction. The authors provide several baseline experiments, including the common practice of state-tactic tuning and prompting methods (which works for standalone problems as presented in $\\texttt{miniF2F}$) and file-tuning that works under such a context-rich setup.", "questions": "1. Is the 1.3b model in L349 the same as the DeepSeek Coder 1.3b in L343?\n\n2. What is the \"Environment\" in Table 4? Does it stand for the import statements / open namespace statements or something else?", "limitations": "", "rating": 8, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 4, "strengths": "1. The $\\texttt{miniCTX}$ benchmark fills the gap in the current community: it expands current benchmarks by addressing the limitations of standalone theorem proving and enabling evaluation in real-world scenarios where context is critical.\n\n2. I appreciate the authors' commitment to automatically updating the benchmark and maintaining a temporal split to mitigate the data contamination, given that most LLMs nowadays crawl GitHub and train on it.\n\n3. The authors present details for constructing the benchmark and the sources. The addition of the $\\texttt{miniCTX}$ and the NTP-TOOLKIT will be valuable assets to the community. The authors also present solid baselines in Table 3 using inference-time methods with GPT-4o and fine-tuning methods using 1.3b model. An ablation of providing different contexts is also presented in Table 4 to show the source of gain from each context component.", "weaknesses": "1. $\\texttt{miniCTX}$ does not have a valid/test set separation. Though it's not inherently an issue for a benchmark, separating a valid set could make the benchmark less gameable under Goodhart's law.\n\n2. It seems that some problems in $\\texttt{miniCTX}$ are with contexts that could be easily \"in-lined\" and transformed into context-less problems. For example, the example shown in Appendix A.1: one could easily in-line the square function $s$ definition into the lemma s\\_eq\\_pow\\_two and make the statement to be $x * x = x ^ 2$ from $s \\ x = x ^ 2$. The same in-line transformation seems to be also applied to the example in Appendix A.2 by inlining the Rectangle definition. It would be great for the author to assess how many problems in $\\texttt{miniCTX}$ could be transformed into context-free problems under certain efforts.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "AlpMGTgtHi", "reviewer": "Reviewer_uXMR", "summary": "This paper introduces a new benchmark called miniCTX for evaluating a model's context-dependent theorem proving abilities, i.e., a model's ability to maximize Expectation_{(theorem, context) ~ repository} Expectation_{proof ~ model(. | theorem, context )} [theorem is valid proof in context]. In-file context includes the source code that precedes the theorem in the file while cross-context includes the in-file context and relevant premises from imported modules. The authors argue that this is a more realistic evaluation of a model's theorem proving abilities. Additionally, the paper introduces NTP-toolkit, a tool for constructing/extending miniCTX with future repositories and running baseline evaluations.", "questions": "- The weaknesses section contains questions that I'd be curious to hear the answers to.\n- Why doesn't the cross-file context include the source code of imported modules as opposed to just the premises? Is this just because of context-length limitations?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The paper introduces a useful tool (NTP-toolkit) and benchmark (miniCTX) for evaluating a model's theorem proving capabilities. The Python Lean REPL, provided that it is performant, is another useful component that will enable researchers to more easily evaluate models.\n- A benchmark of context-dependent theorem proving and a model that performs well on it could potentially be useful for assisting humans using Lean for formal verification.\n- The idea of file tuning, i.e., training model(tactic | theorem, context) is novel.", "weaknesses": "- The differences between benchmarks shown in Table 1 is, in my perspective, superficial. For example, what fundamental reason is there from preventing other theorem-proving extraction tools from extracting a timestamp or saving the file name that a theorem is extracted from?\n- There seem to be a few missing experiments. First, since the temporal split is emphasized, is there any empirical evidence to support the failure of other benchmarks to handle this properly? Second, for file-tuning, have other LLMs / those fine-tuned on Mathlib been tested with file-tuning to see if file-tuning works across different models? Third, In Table 4, I'd like to see context = environment + definition + lemma statement but without natural language comments. This way, we can see just how much having the lemma proof affects file-tuning to better support the claim that models can learn from previous proofs in context.\n-  While the paper offers empirical evidence and some analysis, there isn't much in the form of hypotheses to guide the design of the benchmark or experiments. As an example hypothesis, while it might not be surprising that model(tactic | theorem, context) > model(tactic | theorem) since we condition on more information, we hypothesize that the gains come mostly from context = previous proofs since this offers the appropriate context as to when an automated tactic can be most beneficially applied. Such hypotheses would help guide and focus the experiments, and offer more insight into the success and failure cases of neural theorem proving with LLMs.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "2LTekcgEoC", "reviewer": "Reviewer_jrzz", "summary": "This work propose a new formal theorm proving dataset that tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. This work also reports the baseline results of the miniCTX dataset.", "questions": "Please check the weakness", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "* This work provides a new dataset for the theorem proving, which tests the model's ability to prove formal mathematical theorems that depend on new context that is not seen during training. And the ability to use context is not captured by previous benchmarks such as miniF2F.\n* The work provides baseline results on miniCTX, telling the difficulty of the proposed miniCTX.\n* The work provides detailed analysis on the experiments.\n* The work provides details of the miniCTX dataset and samples in the Appendix, which makes it easy to understand what the miniCTX looks like.", "weaknesses": "* For the Table 3, how do you test the File tuning Model result on miniF2F, as the miniF2F only has the formal statement? You may: 1) only give the formal statement for File tuning Model and get the result; 2) Or, you provide addtional context information by any way?; \n* For Table 3, you do not report the result of GPT-4o (full proof), could you explain why? Previous works (DSP, LEGO-Prover or Lyra) all reports the results GPT-4 on miniF2F.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Oral)