Synthetic Theorem Generation in Lean

W3. Marginal Experimental Results

While the performance improvement from our synthetic data was modest, we believe its consistency provides support for the utility of our synthetic theorems. We note that there are avenues to diversify and enhance the generated data—such as expanding the number of forward-reasoning tactics as they become available in Mathlib, or replacing ReProver with a purpose-built premise-selection model (we selected ReProver for its ease of use and ubiquity in this area, though it is not directly optimized for this task)—that may improve the utility of the generated theorems without modifying the overall architecture of the generator. It is this broader architectural contribution that we believe distinguishes our work; as we noted in our response to item W1 above, there are multiple novel aspects we present in this regard, including our search/synthesis strategy (§§4.2–3), tactic-execution/simulation scheme (§4.1), LLM-based lemma selection (§4.4), and verification pipeline (§4.5).

With respect to your concern regarding ablation studies, we did evaluate the model both with and without synthetic training data, as shown in Table 3. We did not include the performance of the base model without any fine-tuning because its performance was quite poor. We also did not evaluate the model when trained solely on synthetic data because the intent of our dataset is to serve as a complement to existing real-world data, providing additional examples of key reasoning strategies in Lean, but not as an all-encompassing corpus of Lean/Mathlib reasoning tactics. Since our synthetic theorems are targeted in this manner, they are not designed to be the sole source of training data for a model.

We appreciate your comment that your evaluation of our data would be aided by assessing the newly proved theorems. To this end, we have added in Appendix G examples of theorems proved with but not without synthetic training data: as these demonstrate, the newly proved theorems are from multiple distinct domains and use a variety of tactics. Moreover, the performance of models fine-tuned with synthetic data consistently exceeded that of models fine-tuned only on Mathlib, supporting the efficacy of the synthetic data.

W4. Nit: Figure 1, which explains basic background information, feels unnecessary. It would be more useful to include examples of the synthetic datasets or newly proved theorems… Additionally, in Table 1, the label for the number of random premises seems to be fractional, but it’s listed as a percentage (%) in the row title, which could be misleading.

We appreciate your suggestion regarding the addition of examples of synthetic theorems and newly proved theorems, and we have added these to Appendices F and G. We have added a figure with a concrete example of a synthetically generated theorem, per your suggestion, and have moved the former Figure 1 to an appendix. Thank you also for catching the discrepancy in Table 1; we have corrected this error.

Q1. Could you conduct experiments or analysis to evaluate the quality of the synthetic datasets? For instance, how does the LLM perform when fine-tuned solely on the synthetic data? Additionally, could you compare the performance of a model fine-tuned on an equivalent-sized synthetic datasets to one trained on the real-world datasets?

The intent of our dataset is to serve as a complement to existing real-world data, providing additional examples of key reasoning strategies in Lean. However, since our synthetic theorems are targeted in this manner, they are not intended to provide an exhaustive treatment of all possible tactics and reasoning strategies that are possible with Lean/Mathlib, and therefore are not designed to be the sole source of training data for a model.

Q2. Could you also provide examples or newly proved theorems from the miniF2F-test, along with the specific tactics the model used to prove them? Additionally, do the theorems proved by the model fine-tuned on the extended datasets…overlap with the theorems proved by its counterpart…?

We have added in Appendix G several examples of theorems that were proved by a model fine-tuned on the synthetic datasets but not proved by the same model fine-tuned only on Mathlib. To specifically address your second question, there were also theorems proved by the model fine-tuned only on Mathlib data that were not proved by the model fine-tuned on synthetic data—neither set of proved theorems (with synthetic fine-tuning data or with Mathlib-only fine-tuning data) was a subset of the other.

We thank the reviewer for their detailed feedback and suggestions. We respond below to the concerns and questions raised:

W1. Lack of Technical Novelty in Synthetic Theorem Generation

We respectfully disagree with the conclusion that our work lacks novelty. We outline the novel aspects of our contribution below. Firstly, we are the first to realize such a system of forward-reasoning-based theorem synthesis in Lean's tactic mode, as also noted by reviewer tn5n. Since the majority of human-authored Lean proofs are written in tactic mode rather than as raw terms, this results in training data that is significantly more relevant to real-world proof tasks. Secondly, our approach is not restricted to a single mathematical domain, but is broadly applicable across the fields of math formalized in Mathlib, which represents a wide swath of modern mathematics. Lastly, we enhance our theorem synthesis procedure with LLM-based premise selection, which allows our tool to select relevant library lemmas across this broad array of mathematical disciplines, improving both efficiency and the relevance of the output theorems.

W2. Potential Limited Diversity and Difficulty of Generated Theorems

While our current generator configuration uses five or seven tactics (depending on whether proof minimization is enabled), it is more extensible and capable of generating more diverse theorems than this may suggest. First, tactics can take arguments that significantly broaden the types of reasoning they can apply. The have tactic alone can apply more than 150,000 lemmas in the Mathlib library, which span much of modern mathematics. Secondly, our generator is extensible with additional forward-reasoning tactics—our architecture does not rely on the specific behavior of the five we selected. The number of forward-reasoning tactics available in Mathlib is currently limited, and we sought to choose a robust subset whose functionality did not overlap, but more forward-reasoning tactics can be easily added to the generator in cases where a premium is placed on the breadth of tactics used.

We also believe that our synthetic theorems do exhibit diversity in several respects. Firstly, we promote diversity in the proofs we generate using the algorithm shown in Figure 3, which ensures that proofs diverge from one another as early as possible. Secondly, we generate theorems using initial proof states from across Mathlib, leading to synthetic theorems that address a wide array of subject areas in mathematics. We have added a table in Appendix H that lists the number of theorems in our synthetic dataset generated using initial states from each top-level Mathlib submodule (e.g., Algebra, Analysis, Topology), illustrating this subject-matter diversity. The theorems can also exhibit user-specified degrees of complexity, since the number of reasoning steps they employ is configurable in the generator and can be set to arbitrarily large values. With regard to your final concern in this item, we have also added examples of synthetically generated theorems in Appendix F.

W2. The paper does not provide specific metrics or validation methods to assess the quality or relevance of the generated synthetic theorems.

We appreciate the reviewer's concern about quality assessment of the synthetic theorems. While we acknowledge that developing comprehensive quality metrics for theorem generation remains an open research challenge, we provide several concrete measures to assess our approach:

First, the coverage table presented in Appendix H serves as a quality indicator. This table demonstrates how our synthetic theorems span different mathematical fields, providing a quantitative measure of the diversity and relevance of the generated content.

Second, we compare the complexity of proofs that M1 can generate with and without synthetic data fine-tuning. Our results show that models trained with synthetic data are capable of producing more complex proofs. This serves as a proxy measure for the quality and utility of the synthetic training data.

Third, one metric we already recorded in our initial experiments—as displayed in §5.1—is the mean length of the output proofs. Since each line corresponds to an additional reasoning step required to deduce the conclusion from the assumptions, this metric serves as a proxy for the complexity/difficulty of the proof. Because the desired range of generated proof lengths is configurable, the generator is capable of creating proofs of effectively arbitrary complexity with respect to this metric.

We agree that developing more sophisticated quality metrics for synthetic theorems is an important direction for future research. However, this represents a broader challenge in the field of automated theorem proving that extends beyond the scope of our current work. Our focus in this paper is on demonstrating the practical utility of our synthetic approach through measurable improvements in model performance.

W3. The generation process requires significant computational resources

While our experimental setup did require significant computational resources, these can be reduced by modifying the generator’s configuration, such as using fewer premises or disabling re-elaboration during the verification phase. Additionally, the process of proof search frequently yields diminishing returns: initially, easy-to-synthesize proofs are rapidly produced; later, as the generator is left to find more challenging proofs (e.g., ones where premise selection yields many “near-miss” lemmas or in Mathlib modules with large numbers of proof steps that yield few proofs), the rate of proof production slows considerably. We observed this repeatedly in our experiments. Therefore, we anticipate that one could generate a significant fraction of the proofs we produced without extensive computational resources. Moreover, our experimental setup was batched, such that we could not granularly determine whether all vCPUs remained in use for the entire 24 hours; it is possible that certain machines with long-running tasks continued while those that had completed theorem generation sat idle, which would yield an inflated account of our resource utilization.

Q1. …are there any metrics or quality checks in place to evaluate the significance and validity of the generated theorems and proofs beyond their correctness by construction?

Please refer to our response to item W2 above.

Q2. Which specific theorems in miniF2F were newly proved by the Falcon2-11B model fine-tuned with synthetic data? These examples could help clarify the types of problems that benefit from synthetic training.

Thank you for this suggestion. We have provided below a few examples of newly proved problems from minif2f. We have also added Appendix G, which includes full newly-proven theorems and their proofs from a model fine-tuned on synthetic data.

theorem mathd_algebra_263
  (y : ℝ)
  (h₀ : 0 ≤ 19 + 3 * y)
  (h₁ : Real.sqrt (19 + 3 * y) = 7) :
  y = 10

theorem amc12a_2002_p6
  (n : ℕ)
  (h₀ : 0 < n) :
  ∃ m, (m > n ∧ ∃ p, m * p ≤ m + p)

theorem mathd_algebra_113
  (x : ℝ) :
  x^2 - 14 * x + 3 ≥ 7^2 - 14 * 7 + 3

theorem induction_11div10tonmn1ton
  (n : ℕ) :
  11 ∣ (10^n - (-1 : ℤ)^n)

We thank the reviewer for their in-depth feedback and suggestions. We respond below to the concerns and questions raised:

W1. …the fine-tuning of these theorems leads to only a modest improvement in miniF2F performance…notably lower than state-of-the-art approaches such as DeepSeekProver v1.5 and InternLM Prover v2.5, which achieve over 60% on miniF2F dataset.

While our particular experiments did not achieve the same performance as SOTA approaches like DeepSeekProver and InternLM, there are several factors that contribute to this disparity; because of this, and because of the more broadly applicable nature of our work, we believe our contributions are still significant despite these differences in absolute performance.

• As we elaborate upon in our response to item Q3 below, our focus was not on the architecture of our final proof-search model but rather on the synthetic theorem generator itself. Accordingly, we opted to build and fine-tune a proof-search approach representative of common prior work; our architecture was a parallelized version of that used by LeanDojo. Thus, it was expected that our performance would not match that of SOTA architectures like those used by DeepSeekProver and InternLM; instead, we aimed to show that synthetic data could be successfully employed to improve theorem-proving ability, which we believe the data in §5.2 evince.

• As we note in §6, the diversity of our generator’s output could be further enhanced with expanded forward-reasoning capabilities in Mathlib. Our generator is capable of supporting a wide range of forward-reasoning strategies; currently, though, there is a relative paucity of strictly forward-reasoning tactics in Mathlib. This is not a restriction of our generator per se, but rather reflects the fact that many tactics in Mathlib operate exclusively or partially backward. However, many backward-reasoning simplification and rewriting strategies can be adapted to forward reasoning by performing the same operations at a hypothesis instead of a goal (this is how we were able to employ typically backward-reasoning tactics like rewrite and simp in a forward-reasoning manner). Therefore, if and as more forward-reasoning functionality is added to Mathlib, our generator could produce more varied theorems, equipping LLMs to reason using a wider range of tactics, while using the same architecture we have already presented.

• As we note in §§4.4 and 6, we relied on the LeanDojo ReProver model—which is limited compared to SOTA—for premise selection. We selected this model for its ease of use and the fact that it was trained on a related—but not precisely aligned—task. A more powerful or purpose-designed model could suggest more relevant theorems, producing proofs that more robustly demonstrate the effective use of both library lemmas and built-in tactics. Nonetheless, we believe the positive results we saw even using the ReProver model provides evidence for the utility of our approach irrespective of the additional benefit conferred by the selection of premise-selection model.

Moreover, our primary contribution is our novel architecture for generating synthetic training data through forward reasoning in Lean, including a diversity-optimized search strategy (§§4.2–3), lightweight tactic-execution/simulation scheme (§4.1), LLM-based lemma selection (§4.4), and verification pipeline that accounts for Lean’s significant notational extensibility (§4.5). We believe these contributions, whose efficacy is supported by a modest but consistent performance improvement, still offer substantive benefits for LLM-based theorem proving.

Q3. Could this approach be modified or enhanced to better align with the needs of SOTA theorem-proving systems, potentially addressing the disparity in miniF2F performance compared to SOTA models? Is there any specific reason to use Falcon2-11B compared to other models?

We believe that our techniques are applicable to a wide range of models that require formal theorem statements and proofs in Lean for training. There is nothing specific to our synthetic generation approach that requires our specific model architecture.

Our intent was not to focus on the architecture of the proof-search model itself, but rather on the relative impact of these synthetic data compared to training with organic data alone. Therefore, for our experiments, we opted to use a proof-search architecture representative of many commonly employed in prior work, even if this does not match the precise architectures of the latest SOTA systems. We use the same proof search algorithm as LeanDojo [1], with the only modification being that we implemented a parallel version of it. Since synthetic data did improve theorem-proving performance in this setting, we believe our synthetic generator would also be beneficial in SOTA theorem-proving systems, since, as noted, no aspect of the synthetic data is tied to our particular model configuration.

We opted to use the Falcon2-11B model mainly because of our familiarity with the model and the fact that it is one of several open-sourced SOTA pre-trained LLMs. However, our methods are not specific to the Falcon model, and these same techniques could be leveraged to fine-tune other LLMs as well.

Q4. In Appendix B, you assumed a TacticsFor function in Algorithm A that returns a set of applicable theorems at a proof state. How is this function implemented?

The TacticsFor function is straightforward and not computationally intensive, which is why we elected not to give explicit pseudocode; however, we have now added additional details to Appendix B to clarify this function’s behavior. To address your specific concern, it does not iterate over all possible arguments to the selected library lemmas. Instead, in the stream of tactics to apply, we represent have tactics simply by the library lemmas that the generator will attempt to apply; the generator only attempts to fill in the arguments to those lemmas when "executing" the tactic (i.e., line 1 of Algorithm 2)—this is the computationally expensive step in the procedure.

[1] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem prov- ing with retrieval-augmented language models. In A. Oh, T. Naumann, A. Glober- son, K. Saenko, M. Hardt, and S. Levine (eds.), Advances in Neural Information Pro- cessing Systems, volume 36, pp. 21573–21612. Curran Associates, Inc., 2023.

Q4. In lines 115–116, I believe the references "(An et al., 2024; Polu & Sutskever, 2020; Zombori et al., 2021)" are misplaced. These do not pertain to methods used for generating theorem statements.

We appreciate this detailed feedback. Indeed, the citation of Polu & Sutskever here was misplaced, as we only intended to cite this work in the subsequent paragraph; in their §4.6, those authors discuss procedures for generating random theorem statements in the domains of $n$-digit arithmetic and ring algebra using a forward-reasoning-based approach. We believe that the citations of An et al. and Zombori et al. in their current location are relevant, as each paper discusses (though not as its primary contribution) a method of generating known-true theorem statements within a fixed domain:

• An et al., 2024: §3 describes a procedure for generating theorem statements in intuitionistic propositional logic.
• Zombori et al., 2021: §4 alludes to a procedure by which arithmetic problems (i.e., theorem statements) are randomly generated; the generator itself can be found in the project repository.

[1] Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, and Jingbo Shang. Learn from failure: Fine-tuning llms with trial-and-error data for intuitionistic propositional logic proving. arXiv preprint arXiv:2404.07382, 2024. [2] Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024. [3] Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024. [4] Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. In Anupam Das and Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, pp. 167–186, Cham, 2021. [5] Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. Training a first-order theorem prover from synthetic data. In International Conference on Learning Representations Workshop on Mathematical Reasoning in General Artificial Intelligence, 2021. [6] 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. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. [7] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020 [8] Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024. [9] Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Advances in Neural Information Processing Systems, volume 33, pp. 18146–18157. Curran Associates, Inc., 2020. [10] Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem prov- ing with retrieval-augmented language models. In A. Oh, T. Naumann, A. Glober- son, K. Saenko, M. Hardt, and S. Levine (eds.), Advances in Neural Information Pro- cessing Systems, volume 36, pp. 21573–21612. Curran Associates, Inc., 2023.

We thank the reviewer for their thorough feedback and suggestions. We respond below to the concerns and questions raised:

W1. The usefulness of these synthesized theorems is a significant concern.

We acknowledge that the absolute increase in the number of theorems proved is limited in our particular experimental configuration. However, our work more broadly presents an architecture for forward reasoning-based tactic-proof synthesis in Lean using a novel search strategy (§§4.2–3), lightweight tactic-execution/simulation scheme (§4.1), LLM-based lemma selection (§4.4), and verification pipeline that accounts for Lean’s significant notational extensibility (§4.5). We believe that these broader architectural contributions to theorem synthesis, in conjunction with our experimental findings that show a modest but nonetheless consistent improvement in performance, still provide substantive benefits for synthetic data generation. Indeed, there are several factors unrelated or nonessential to our general architecture that likely impacted our experimental results:

• As we elaborate upon in our response to item W2 below, the number of forward-reasoning tactics in Lean/Mathlib is currently limited, which does prevent us from generating certain types of proofs (e.g., structured induction proofs) that might provide useful training examples. While, as we note in our response to W2, our existing tactics do still offer diverse reasoning strategies. The various potential extensions of our tactic inventory we discuss in that response could increase the utility of the synthesized theorems—using the same architecture we have presented here.

• As we note in §§4.4 and 6, improving the model used for premise selection could lead to more relevant theorem selection, producing proofs that demonstrate the effective use of both library lemmas and built-in tactics. While we rely on ReProver because it is trained on a related task and works easily out-of-the-box, it is not—as we note in §4.4—specifically trained for this task and, as a result, may produce less relevant lemma suggestions than a purpose-built LLM. Even so, the positive results we saw even with the ReProver model suggests the efficacy of our general approach, even without the additional benefit of a more powerful premise-selection model.

• For our experiments, we opted to use a proof-search architecture representative of techniques commonly employed in prior work rather than the latest SOTA approaches, since our focus was on synthetic theorem generation rather than proof search. (Our approach was a modified version of that used by LeanDojo ReProver [10].) Accordingly, its performance was constrained relative to SOTA works.

We thank the reviewer for their thoughtful feedback and suggestions. We respond below to the concerns and questions raised:

W1. …it seems the authors have not established a robust metric to assess the diversity of the generated theorems or to quantify how this diversity impacts the performance of fine-tuned neural provers.

We appreciate your observation of the importance of our search algorithm to our work’s contribution. We did not perform a post-hoc assessment of theorem diversity because there are two relevant but somewhat orthogonal notions of diversity, both of which are principally controlled by the configuration of the generator prior to generating synthetic theorems and for which there does not appear to be consensus on clear evaluation metrics. However, we have added an additional metric regarding subject-matter diversity, which we explain below.

The first relevant notion of diversity is the diversity of the proofs themselves. The algorithm in Figure 3 promotes this type of diversity by ensuring that proofs diverge from one another as early as possible. Because this is the case, there is little room to further promote diversity in the search algorithm itself, since any other algorithm could only produce proofs with greater overlap among them.

The second relevant notion of diversity is the diversity of the subject matter of the theorem statements themselves—i.e., the mathematical fields to which they apply. To promote this form of diversity, we ran our generator over a large number of Mathlib modules, representing a wide array of modern mathematics. Since the generator draws its initial proof states (including the initial hypotheses from which the generator reasons forward) from these modules, the theorems it produces will span many mathematical disciplines. To further quantify this diversity of topics, we have added a table in Appendix H displaying the number of theorems in our synthetic dataset generated using initial states from each top-level Mathlib submodule (e.g., Algebra, Analysis, Topology).

W2. …it would be beneficial to include more comparisons between autoformalization and the proposed synthetic approach.

We appreciate the reviewer’s questions about comparisons between autoformalization and our synthetic approach. We would like to clarify a key point about the relationship between these approaches: Our synthetic method is complementary to and can be applied to any proof dataset, whether human-written or autoformalized. Rather than viewing these as competing approaches that need direct comparison, our method serves as an enhancement that can augment any existing proof corpus.

In our experiments, we demonstrated this versatility by successfully generating synthetic corpora from both human-written proofs (the Mathlib dataset discussed in §5.1 and Tables 1–2) and autoformalized proofs (the Lean Workbook dataset used for the experiments in §5.2 and Table 3). In both cases, fine-tuning on the synthetically expanded datasets led to improved model performance compared to fine-tuning on the original datasets alone.

The empirical results suggest our method provides value regardless of the proof source, making direct comparisons between autoformalization and synthesis less relevant to evaluating our contribution. The more pertinent comparison is between models fine-tuned on a given dataset with and without our synthetic augmentation—a comparison our experiments directly address.