TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
Authors: Jing Xiong
Jianhao Shen
Ye Yuan
Haiming Wang
Yichun Yin
Zhengying Liu
Lin Li
Zhijiang Guo
Qingxing Cao
Yinya Huang
Chuanyang Zheng
Xiaodan Liang
Ming Zhang
Qun Liu
Venue: EMNLP 2023 Main (2023)
Keywords: Trigonometric Expression Reduction
Automated Theorem Proving
Formal Mathematical Proof Reduction
Complex Number Combination Reasoning
Generative Language Models

Abstract: Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful  
generative language models. However, current ATP benchmarks are mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proof but also evaluates a generative LM's reasoning ability on formulas and capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from web, annotate the simplification process manually, and translate it into the ``Lean'' formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we also create three automatically generated training and testing datasets of varying difficulty and distributions. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.

Trigo: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
Jing Xiong'; Jianhao Shen?; Ye Yuan', Haiming Wang', Yichun Yin Zhengying Liu Lin Li Zhijiang Guo Qingxing Cao Yinya Huang 1.4
Chuanyang Zheng", Xiaodan Liang'; Ming Zhang"; Qun Liu
Shenzhen Campus of Sun Yat-Sen University ?Peking University
Thhe Chinese University of Hong Kong "City University of Hong Kong
SSun Yat-Sen University HHuawei Noah's Ark Lab
lxiongj69, wanghm39, caoqx)@maille
(ihshen, yuanye_ mzhang) @pku.
(yinyichun, 1iuzhengying2, guozhijiang, 1ilin29, qun. (et.lluu@@hee Shuwweluwwwecomm
[cyzheng21) (ttpss2eeecceeeeetee edu. (yinya.el. huang, xdliang329 8gmail.
Abstract
Trigonometric expression
Lean Formlization
2ez
an -
tittpp/31 (27o00 (21/220-12 (2) beggin
Automated theorem proving (ATP) has become an appealing domain for exploring the reason- ing ability of the recent successful generative language models. However, current ATP bench- marks mainly focus on symbolic inference, hut rarely involve the understanding complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires model to reduce trigonomet- ric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplifica- tion process mamually, and tramslate it into the "Lean" formal language system. We then auto- matically generate additional examples from the annotated samples to expand the dataset. Furthermore, develop automatic genera- tor based on Lean-Gym to create dataset splits varying difficulties and distributions in order thoroughly analyze the model's generaliza- tion ability. Our extensive experiments show our proposed TRIGO poses new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem- proving lan- guage data, and provide new tool to study the generative LM's ability on both formal and mathematical reasoning.
(2)
1-811
twe,
die
have 203 los 12
2ond
have (pt/ 2F (PEP1213)
20x
<pe sungr_.tt .erg
33
22 -311
pl
oza
nomm pem
Figure 1: The task of trigonometric expression reduction. The key is to rewrite To into y ((he green part), and apply the half-angle formula (the orange part). Both steps need understanding of numbers and formulas.
flexible reasoning and is easy to validate, making it an appealing domain for exploring the reasoning ability of the recent successful pre-traine pre-trained genera- tive language models. These models show strong proof generation capabilities (Lample et al., 2022: Jiang et al., 2022), but its ability to perform formal mathematical proof reduction, which involves com- plex numerical reasoning, has not been thoroughly explored.
Current ATP benchmarks (Wu et al., 2021a; Han et al., 2021; Zheng al., 2022) mainly focus on symbolic inference but rarely involve the under- standing of complex number combination reason- ing, such as term grouping, term factorization and equivalent substitution. For advanced mathemati- cal proving such as trigonometric expressions, ATP can be beneficial for evaluating the crucial com- plex number combination. For example, as shown in Figure 1, correctly reduce the left-hand-side expression, one must recognize the specific angles or terms such as cos( }. capable of applying the half-angle formula and know the result is cos( (3 ?)
1 Introduction
Automated theorem proving (ATP) requires formal reasoning and deduction from conclusion to axioms or known theorems. This task requires general and
"These authors contributed equally.
*Corresponding author

---

Plaas help prove this problem using Lean: lomma Trigo, O wix(
We reguire lamna from Lean's standard libmay for the proof and to correctness the equation
functions, trigononetzio for
import ansiyole.
Ponctiions, tri.gnnmetrio..ee
open real
ceal
lenas sin pezioiie begtn
win sin 2 pai
Loeale real
Laams Trigo_0 0 2. x1m1:07 X1 =.G
inteco,
begin
extct (55 PoclodAo pá K, -maszzzable in Lean standard Libracy
--tine the perfodictty the sine Funceton:
--add 2e-2 for any inceger
axn(x)
lenns Veigo_0 1107 pá)
periodie Loc
bagin
--Stepii2y right-aand liide have 107
--tto the pezlodieiyy of sin zelate sin pdi singg have h 1 ddn 1107 pP) - ein (1 pll,
2 * -53 I Inra oonn 101, mol_com 541, noma pux ",
Coemane and à toan can the sine of muitipier of
-pplly sin pin_pesiod.e Ie
(h h sin sin_woi pin_wti_p__oo pi_of_ne__om 541,
end
know aimipe)
manailable
libeazy
Figure 2: An example of GPT-4 struggling to solve TRIGO. GPT-4 corrects its response after the second prompt (box in right), but continues generating error tacties (highlighted in red with cross mark).
Such proof steps be automatically denoted by the formal language deduction shown in the right-hand-side, and then verified via the interactive theorem-proving environment in ATP.
tion software to manually label the reduction steps and formalize the processes into "Lean" formal lan- guage. Finally, based on this manually formalized data, we develop an automatic proof generation program to expand the dataset with real-world data and create datasets of artificially generated sam- plcs. Specifically, we generate 3 types of samples by controlling their proof length and generating trigonometric functions with larger numerical val- ues assess the models' ability to generalize out-of-distriben di-sriibbuttinn data.
To develop such profound ATP evaluation for current generative LMs, we propose the task of Trigonometric Expression Reduction (TRIGO). Given a trigonometric expression, a model is re- quired to accept formal input with Lean formal language and then perform step-by-step proof re- duction. The proposed TRIGO poses new chal- lenge for current state-of-the generative LMs. Figure 2 presents an illustrative example of proof generated by GPT-4 (OpenAI, 2023). Inspired by self-refine (Madaan et al., 2023), we first provide the prompt "Please help me prove this problem using Lean: lemma Trigo_0: sin(107 pi) =0 0 :" to GPT-4 and the GPT-4 generates non-exist tac- tics and gives the incorrect equations. We further prompt it with "We require to use lemma from Lean's 's standard library for the proof and to ensure the correctness of the equation" correct the GPT- 4. However, in the second attempt, the GPT-4 still applies the tactic "sin ciin__errodic__ii that does not exist in the Lean standard library and comments "---availalle in Lean standard library". Surpris- ingly, GPT-4 produced the correct equation "have h: sin(107*pi) sin(1 pi)" in the second proof at- tempt, even though the proof for this subgoal is incorrect. This example demonstrates the potential of GPT-4 in accurately manipulating numbers and formulas, as well as the challenge of strict formal reasoning posed by the TRIGO task.
Our contributions are three-fold:
We propose the new trigonometric expression reduction tasks that the first to explore for- mal mathematical reasoning abilities with re- gard to both formulas and numerical elements understanding.
We construct the new TRIGO dataset with manually labeled reduction steps and convert them to the formal language Lean (de Moura et al., 2015). We also generate extra samples with controlled difficulties and distribution to further evaluate different aspects of generative LMs.
We conduct extensive experiments and de- tailed analysis of a broad range of methods, identifying the new challenges for current state-of-the-art generative LMs.
2 Related Work
Automatic theorem proving (ATP) has numerous formal environments such HOList (Bansal et al., 2019a), Metamath (Megill and Wheeler, 2019). and CoqGYM (Yang and Deng, 2019). There are several formal benchmark tasks for theorem prov- ing that exist. LeanStep (Han et al., 2021) extracts (state, tactic) pairs from mathlib (mathlib, 2020), a
To construct the TRIGO dataset, we collect trigonometric expression reduction problems and corresponding answers from high school exercises and exams. We then develop an interactive annota-

---

comprehensive library of theorem proofs in Lean. The IsarStep dataset (Li al., 2021) mines inter- mediate proof steps from the Archive of Formal Proofs (AFP). MiniF2F (Zheng et al., 2022) is a cross-system benchmark of olympiad-level math- ematics problems, containing 488 problems for- malized in Metamath, Lean, Isabelle, and HOL Light, but only small portion has formalized solu- tions. FIMO (Liu et al., 2023) targets formal Inter- national Mathematical Olympiad (IMO) problems. The Geometry3K dataset (Lu al., 2021) includes 3,002 geometry problems with annotated formal language descriptions but lacks interaction with formal environments. Many other works also focus on informal math problem solving (Saxton et al., 2019; Hendrycks et al., 2021; Cobbe et al., 2021; Shen et al., 2021). Our work is most similar to (Wu et al., 2021a). They use formal mathematical reasoning to reduce equations and incqualities and employ programs to automatically generate proofs to explore combinational generalization. However, they lack real-world problems to assess the model's generalization to real distributions and do not in- volve complex numerical operations combination. Compared with previous work (Wu et al., 202 la) which has 18 axioms and 9 transformations, generation process has total of 85 transforma- tion rules and diverse sampled parameters. Our proposed TRIGO generates complex samples with controlled difficulties and distribution, and includes manually annotated samples and proof steps from real-world problems.
1eama tx1ge, exargle kintpt/331 (2to0k1ps/122 tp eageet
PROOUSTER
CT9, pt..pl..c.... 2MC.
GOAL
GOAL -12-2//-22 det 200 2o0 PROOFSTEP
zkng PAp.
Part
Language Model
Formal System
Figure The proof flow is produced the interactive Lean- man--yymon environment. The language model generates proof steps given the formal prompts until reaches "no goal".
mutative (semi)rings. More details of used tactics are given in Appendix H. Lean-Gym (Polu et al., 2023) an interactive environment that allows language models to inter- act with formal systems. As depicted in Figure 3, we begin by acquiring the initial goal state G1 as "} sin( a /33) + 2 cOS(TT /12 (2) *2 cos(:/2) = sqrt(3) + 1 This goal state is inputted into lan- guage model with the prompt "GOAL G1 PROOF- STEP". Subsequently, GPT-2 generates the corre- sponding tactic T₁ as "rw cos cos_pi_diit div_two."" Given the goal state and tactic, Lean-Gym outputs a new goal state "I sin(TT/) + cos( /T/ /2) *
sqrt(3) + 1" for language model to obtain the next tactic. We iteratively perform this process until the Lean-Gym returns "no goals" which indicates the proof is complete.
3 Background Lean Environment
Formal language systems are effective tools for strictly verifying the correctness each proof step generated by the model. In this work, we use Lean (de Moura et al., 2015) as formal environ- ment.
TRIGO Dataset
In this section, we first introduce how we collect trigonometric expression reduction problems from "tiku", annotate the step-by-step reduction pro- cesses, and transform them into Lean formal lan- guage to create the TRIGO-real and TRIGO-web datasets. Then introduce how automatically generate data construct the TRIGO-gen.
The correctness of a given proof can be veri- fied by a Lean verifier program. Lean proof example is shown in Figure 1. It starts from a goal state "I sin(m/3)) 2 cos(T//1)- 2 coS(TT2) = (3)t(3) + 1", representing the current proof goal. In the row next to the "begin", tac- tic "rw cos cos_pi_dii_ dii__two" is applied to the current goal state, meaning rewrites the term cOS(TT/2) to 0. In the following rows, the proof applies "have" tactic generates new sub-goal such as proving cos(m = cos(T/6))/2 2 + 1/2, and applies the "ring_exp" to solving exponents equations in com-
4.1 Problem Collection
We collect the trigonometric expression reduc- tion problems from "tiku", large-scale math problem set from textbooks and exams. Specifi- cally, we collect problems and their answers from 'htps:/wwwwttiku.co/

---

the "'rigonometry" topic. We eventually collect 427 problems and denote them as TRIGO-real. To expand our dataset, we further collect addi- tional trigonometry reduction problems from dif- ferent websites. After manually filterigg the dupli- cate problems, we obtain an additional 453 sam- ples as TRIGO-web and use them as the test set. These data are collected from other websites found through search engines. These sources contain high school math exam questions with standard answers. Throughout the collection process, we aim gather data randomly whenever possible, ensuring diver- sity in the distribution of the test set to reflect the model's performance on real human exam ques- tions.
Identity Rule Name
Example
sin
sin (0)
sin_pi_div_six
sin (g)
cos_pi
cos (f) -1
cos_neg
cos (X) cos (2 K X)
+ san( (X 1-tam(X)=tan((?
tan add
Table I: Examples of our pre-defined rule bank.
the equation and rules into expression trees. Then we compare each equation sub-tree with the rule tree. If two trees are identical except for the sibling nodes' order, consider they matched and the equation valid. Given matched sub-tree, we further use sympy to extract the arguments X, Y, and K. The full list of examples is demonstrated in Appendix I.
4.2 Interactive Proof Annotation
The collected problems have only the final results without step-by-step reduction processes. To facili- tate the annotation of these crucial processes, develop interactive software specifically tailored for this purpose. The annotation process has the following steps:
4.3 Lean Formalization
After obtaining the stepwise reduction annotation, manually transform the annotated equation into Lean formal language. Since we use Lean-Gym with mathlib (mathlib, 2020) backend as our formal environment, Lean-Gym can only accept tacties in- side the mathlib. To ensure the correct acceptance and processing of our defined trigonometric rules in Lean-Gym, we derive these rules from math- lib theorems and convert them into tacties before adding them to mathlib.
Step. 1 The software shows an expression the annotator.
Step. 2 The annotator inputs transformation equation that will be applied in the next step.
Step. 3 The software checks if the equation valid by matching it with rule in a pre- defined bank. If no rule is matched, the software reports "No Matched Rule" and goes back step 2.
We then construct the framework of the proof script. The script begins with the keyword "lemma" followed by name and the premises of the lemma and then presents the goal equation where the left- hand side (LHS) represents the original expression and the right-hand side (RHS) represents its re- duced result. Lastly, we add the "begin", "sorry", and "end" keywords where the "sorry" is place- holder that will be replaced in the following steps. Given the empty proof script, we convert the annotated step into Lean tactics. Recall that dur- ing the annotation phase, each annotated step is matched with a predefined rule, which can be fur- ther converted to a Lean-Gym tactic using a Python program. Thus, we only need to apply the corre- sponding rule with proper arguments parsed by sympy. Take the equation sin ( as example. The matched rule is sin (X) sin (X 2*) with argument
Step. 4 The software applics this transformation to the current problem. If succeeds, the software outputs the new expression. Oth- erwise the software reports "Rule Failed" and goes back to step 2.
Step. 5 Repeat steps 2-4 until the expression equals the answer.
Equation-Rule Matching In step 3, each anno- tated equation must match with predefined rule ensure its correctness. We define total of 85 nules that can cover most of the trigonometric trans- formation. Some examples are shown in Table 1. As shown in Table 1, some rules have value ar- gument X, Y, and parameter K. To perform the rule matching, we first use sympy² to parse both
13r
sin (7)
13t After apply- 6
ing this rule sympy we get new goal equation:
sin 13tt 2 = sin (g), along with the corre- 6 sponding tactics.

---

To obtain the parameter K for some rules such cos(X) sin(2 π X + 2), we uniformly choose an integer between [0, 100) as its value.
Tecttic length density
0.07
1641
TG3
0.06
TRiGD-rea
To control the difficulties of the generated sam- ples, under the assumption that the difficulty of the problem increases as the number of sampled rules grows, we sample and apply 1, 2, and 3 rules to construct TRIGO-gen, denoted as TG-1, TG-2, and TG-3, respectively. For each rule length, we generate 9,000 training samples, 1, 1,000 validation samples, and 1,000 test samples. To close the gap between the generated samples and real-world sam- ples, we also use the trigonometric expression in TRIGO-real as initial goal expressions G, then sam- ple and apply the exact 3 rules to generate the set TG-E as generated training data.
IG-6
0.05
Proportion
0.04
0.03
0.02
0.01
0.00
150
Tactic lingth
Figure 4: Tactic length distribution based on the number
of tactics.
Although the above step can complete most of the transformation to Lean, we still need to manu- ally fix the Lean proof. For example, Lean does not reduce the above new goal state sin 113m - 2x) to
4.5 Data Statistics
Finally, the TRIGO-real has 427 problems and a total of 10,574 proof tactics. We divide TRIGO-real into train, validation, and test splits with 7:1:2 ra- tio, resulting in 299 training samples, 42 validation samples, and 86 test samples. The average proof step size for TRIGO-real, TG-1, TG-2, TG-3, and TG-E are 37, 22, 35, 49 and 81. Since Lean-Gym only accepts one tactic at a time, the tactic length of each problem in the dataset typically matches the size of the proof step. Figure displays the sample proportions concerning their tactic length. We can observe that the generated samples have similar tactic lengths, while the real-world data has various but more uniform lengths. More statistics are in Appendix G.
sin (g), and rewriting tactics "rw sin (z) =
as Lean can not match sin(x + 3) with sin + 2)).
fails when applied to "sin(y + x)... =
Thus, we manually add more steps such that the Lean-Gym correctly process the entire proof.
4.4 Generated Data
To comprehensively analyze the performance of models across various levels of difficulty and dif- ferent ranges of numbers, as well as to study the gap between generated and real-world data, we automatically generate trigonometrie prob- lems and proofs by applying random prede- fined rules repeatedly. Specifically, we randomly choose a rule denoted as from our prede- fined rule bank and select corresponding value arguments X and Y from the value list C = {2TT, n. 2. 3: -3. -T, -2x}, and ini- tialize K with an integer value between 0 and 100, to construct our initial goal expressions G. Then at each step, sample and try to match the with LHS or RHS of goal expressions G. If either side is matched, we replace the corresponding part of goal expressions G with rule r's corresponding Lean tactics set.
Baseline Models
Recent works utilize GPT-based language models for automated theorem proving and have made sig- nificant improvement (Polu and Sutskever, 2020; Han et al., 2021; Polu et al., 2023; Jiang et al.. 2022; Zheng et al., 2023). In this work, we use GPT-2 (Radford et al., 2019) with proof search algorithm baseline method for dataset.
Data Preparation The Lean-Gym (Polu et al., 2023) provides an interactive formal environment to obtain a new goal state given the previous state and tactic, as shown in Figure 3. During training, at each step, we obtain the (state, tactic) pairs from Lean-Gym and training samples respectively, and concatenate them into sequence with the "GOAL" and "PROOFSTEP" special tokens:
During the replacement, we need to determine the value arguments X, Y. and K given the goal G. For example, consider the expression sin( 3m)) and the rule sin (X + y) sin (Y) cos (X), where the argument X Y must 35 equal 4. We first sample the value of from the value list C, then calculate the Y 3x X. 4
sin (X) cos (Y) +
GOAL (state) PROOFSTEP (tactic).

---

Manual Laheling
TRIGO gen
Manual Labeling
TRIGO gen
Model
Model
TRIGO real
TRIGO web
TG-1
TG-2
TG-3
TRIGO real
TRIGO web
TG
TG-2
TG-3
GFT-2a
12.79
13.90
42.79
7.49
0.39
Thaining
GPT-2-
12.79
13:02
71.59
23.39
GPT-2p
9.30
0.94
9.89
3.39
GPT-2--PACT
32.55
25.60
77.29
44.19
18.99
GPT-2,
5.81
0.88
14.29
6.19
2PT-2,,-PM PACT
5.81
0.88
16.39
6.29
GP
17.44
17:21
42.29
12.69
4.89
-P
19.76
20.08
54.79
20.89
7.69
Thaining 7G-2
GPT-2-PACT-L
23.25
25.29
GPT-2p
3,48
0.44
19.59
2.59
-PCCTE-PACTE
34.88
25.38
GPT-2,
4,68
0.66
32.29
8.29
-PCCT
5.81
1.32
48.49
15.89
Table 2: Pass rates of benchmark models and baselines.
Training TG-3
GPT-2p
0.00
5.59
0.89
GPT-2,
0.00
0.00
10.59
3.49
GPT-2, PACT
8.13
1.10
57.19
46.39
We take the above sequence as input and train the GPT-2 models to predict the "tactic" sequence with autoregressive loss (Bengio et al., 2000):
Table Pass rates of models on OOD test set.
the impact of generating data distributions beyond those observed in real-world data. Additionally, we conduct a comprehensive analysis of the models, including an evaluation of GPT-4's performance.
C3 (0) logp (1141l T3; 0;;0),
where / indicates model parameters, and m; is the i-th token of the input sequence:
6.1 Implementation Details
Proof Search After training GPT-2 to generate a tactic given goal state, we search the complete proof by expanding the most probable state each step. We employ Breadth-First Search (BFS) in this paper. Specifically, we define the probability of the goal state as the cumulative logarithm probability its corresponding generated tactics:
All models are trained with Adam opti- mizer (Kingma and Ba, 2015), learning rate of 2.5 10 batch size of 512, and cosine schedule. More implementation details of these models are demonstrated in Appendix A.
6.2 Main Results
Table 2 presents the pass rate of different mod- els on TRIGO-real (training, validation, and test sets), TRIGO-weh (test set only), and TRIGO-gen (training, validation, and test sets). The pass rate indicates the percentage of problems that a model outputs correct proof within the maximum search steps by interacting with Lean-Gym. All models are trained and evaluated on the corresponding training and test splits, except for the TRIGO-real which the models are trained on TRIGO-real training split and tested on the TRIGO-real test split and TRIGO-web.
log Pstatey log Pstatey-1
log Piactieses
where Ptactics, is the tactic's probability generated by the GPT-2. Lean-Gym outputs the new state staten by applying the lactics, to previous goal state slatex-1. At each proof search step, we se- lect goal state with the highest probability and feed the sequence "GOAL (state) PROOFSTEP" into the trained GPT-2 to generate the tactics. We sample 8 tactics based on GPT-2 output probability. The generated tactics with the goal state are input to Lean-Gym to obtain a new valid goal state possible. We repeat the search process until "no goal" state is reached, the queue becomes empty, reach the maximum search step 512.
In Table 2 we find that: (1) Models with different parameter sizes (GPT-2g, GPT-2L) achieve similar performance both TRIGO-real and TRIGO-web when trained the smaller dataset TRIGO-real. On TRIGO-gen that has more training samples, larger model parameter scales lead to better performance; (2) GPT-2,,PACCT achieves the best results on each test set, indicating the significant improvement of pre-training on PACT and raising the question of whether we achieve similar improvement if fine-tune TRIGO-gen.
6 Experiment
In this section, we evaluate the performance of GPT-2BASE (GPT-2B). GPT-2 (GPT-24),, and PACT,, GPT-2LARGE pre-trained the formal proof dataset PACT (Han et al., 2021). Furthermore. we evaluate the model's out-of- distribution generalization ability by examining its performance across various levels of difficulty and different ranges of numbers, while also evaluating
To study the above question, we merge the gen- erated dataset TG-1, TG-2, and TG-3 training split to fine-tune GPT-2p. GPT-21, and further train UPT-2,-PACT, We denote the resulting models as

---

GPT-2B D. GPT-21. D. and -PI-2,-PACT-D and evaluate their pass rate. We find that only GPT-21- PACT-D pre-trained on PACT can obtain significant improvement on TRIGO-gen. However, when we continue to train GPT-2,-PACT-D on TRIGO-real, the performance does not improve significantly, achieving accuracies of only 23.25% and 13.02% on TRIGO-real and PRIGO-web, respectively.
all
w/o have
Dataset
EM@1
EM@8
EM@
EM@#
TRIGO-rcal
69.81
78.40
80.81
86.85
TG-1
92.22
97.31
94.33
98.56
TG-2
89.29
93.71
93.11
96.22
TG-3
86.13
90.36
90.77
93.65
Table 4: The single step performance of GPT--2LPPACT on different datasets. EM@k represents the exact match scores of the top-k generated tactics.
To explore the gap between TRIGO-real and TRIGO-gen, we train the -PCCT on TG-E whose samples are generated start with expression in TRIGO-real. The results are denoted as GPT- 2, P.CT-E. Compared with GPT-2,, -PACT, GPT- 21 PACT-- achieves a 2.33% improvement on the TRIGO-real test set but 0.22% decrease on TRIGO- web. These results suggest that solely increasing the proof length in the training data using genera- tion program does not enhance model performance on the TRiGO-web. We posit that this due the significant distribution gap between TRIGO-real and TRiGo-web, making it challenging for the data generated based on TRIGO-real to generalize to TRIGO-web.
Model
TG-1
TG-2
TG-3
TRIGO-real
PACT
90.23
85.77
81.27
45.40
GPT-4
16.91
7.44
4.67
0.26
Table 5: Exact match scores of single step performance on "have" tactic. We obtain a tactic with highest proba- bility from GPT-2L-PACT, and provide GPT-4 with an 8-shot prompt (randomly sampled from the (state, tac- tic) pairs in the training that contain "have" tactic).
ground truth and consider the model is correct if any of the generated tacties is an exact match with the ground truth. The results are shown in Table 4. GPT models achieve high performance on tactics without the "have" tactics, with EM scores above 86% for the top 8 generated tactics. However, the prediction of "have" tactics poses significant chal- lenge in overall proof generation, especially in the TRIGO-real dataset where there is an 8.45% gap in EM@8 between "all" tactics and tactics without the "have" tactics. In the TRIGO-gen dataset, the gap in EM@8 between "all" tactics and tactics without the "have" tactics increases as the number of proof steps increases.
To investigate the cattof-distributtin generaliza- tion ability on datasets of varying difficulty, we present the results in Table 3. Table 3 shows the results of only training model TG-1, TG-2, and TG-3 and testing on other test sets with different distribution. is shown that all models perform consistently worse than the in-distribution setting. On TG-1, the best GPT-21,PACT trained on the more complex TG-3 dataset is still 20. 1% lower than that trained on TG-1 alone. On TRIGO-real and TRIGO-gen however, model GPT-22-PACC trained with three generated datasets separately per- form worse than the GPT-2,-PACT-E PACT-E trained on the TG-E. This demonstrates that initiating the au- tomatic theorem generation program with input derived from real-world data effectively bridges the distribution gap between real-world data and generated data.
To explore the impact of model size on the ac- curacy of single-step proofs, we evaluate GPT-4, We believe that LLMs such as GPT-4 have already demonstrated their ability to process formal lan- guage, particularly in translating informal proofs to formal proofs (Jiang et al., 2023; Wu et al., 2022). Furthermore, LLMs have demonstrated promise in theorem proving using proof assistants such Lean, evidenced by Yang al.'s study (Yang et al., 2023). The study showed that GPT-4 could generate proofs accepted by a zero-shot manner, thus establishing GPT-4 as a robust baseline. These results suggest that GPT-4 may have been trained on Lean examples, as there were publicly accessi- ble proofs on GitHub prior to GPT-4's data cutoff date in September 2021 (OpenAI, 2023).
6.3 Model Analysis
In this section, perform comprehensive anal- ysis of GPT models
TRIGO with various settings. We mainly evaluate the PACT pre-trained model it achieves the best overall performance. Stepwise Evaluation We first evaluate the single- step generation performance. We obtain all (goal state, tactie) pairs, and select the pairs whose tactic is not "have" as set w/o have. We compare the model's t and top-8 output tactics with the
We also evaluate the single-step performance of GPT-4, focusing specifically on the "have" tactics. Since the "have" tactic only requires generating the

---

Goal
GOAL cos (433-p1/33
GOAL ho (an &
GOAL sint4rpi xo08 (p//3)
this tanl-p1/9)
2+cos (p1/6] ++2
(-10/tee11255pip/
2-ain =coss///22
PROOPSTEP
+ ain("p1/33 (tcpppp//////aaaa//1 (-p1/33
PROOFSTED
can (-p1/3) PROOPSTEP
GPT-4
have:
cos (2+p1/3) (pi/6)
have: sint pi/31 /ooe pi/3:
have: sin (in(4p1/3) -co8 (p1/3)
ICL
tan pi/3),
sin(pi/3) soos (Mpi/3)
2eain (pl//1 +00s (p1/2),
GPT-4
have:
cos (433+pi/3) =
have: can (pt///
have: (2n(2))4) =in(
Instruction
co8 (433 and xpi/3)
tan (113113pp//3)
GT
have: cos tpi/3/
have: sind pi/31 foos pi/31
have: sin(pi)
cos (433xp1/31,
tan (-p1/33)
sin (4. /oo (p1/31
sin (40pp/1//3)
Table 6: One-step proofs generated by GPT-4 given in-context learning (ICL) or natural language instruction (Instruction) and new goal (Goal), compared with the ground truth (GT).
sub-goal equation without additional Lean knowl- edge, evaluating GPT-4's performance these tactics effectively reflects its ability in complex number combination reasoning. For each genera- tion, we randomly select 8 (goal state, tactic) pairs from the training set as in-context learning exam- ples for GPT-4. Table 5 presents the exact match scores obtained. The experimental results highlight a significant performance gap between GPT-4 and the fine-tuned smaller GPT-2 models across all set- tings. Table 6 showcases several one-step proofs generated by GPT-4.
Monual I Labeling
TeinO-gen TG-2
Decoding Method
TRIGO-neal
TRIGO-web
TG-1
TG-3
Beam Search Sampling
23.25
20.75
68.
68.49
38.39
6.79
32,55
25.60
77.29
44.19
18.99
Table 7: Pass rate different decoding methods.
Manual Labeling
TRIGO-gen TG-2
Temperature
TRIGO-real
TRiGO-web
TG-1
TG-3
1.0
32.55
25.60
77.29
44.19
18.99
1.25
31.39
26.49
77.49
45,99
18.59
1.5
29.06
22.07
76.49
44.89
17:39
Table 8: Pass rate with different sampling temperatures.
forms significantly worse than BFS on the artifi- cially synthesized dataset TRIGO-gen, We suppose this is due to the lack of a well-developed value function that should be addressed in future work.
Search Evaluation We conduct three experi- ments to study the effects of tactics decoding and proof search methods.
We first compare beam search and sampling. When generating tactics, we apply beam search with size 16 and expand the proof goal with the top-8 tactics. As for sampling, we randomly select each token based on the model's output probability and sample tactics. Table shows the proof pass rate, and sampling achieves better performance. Af- ter inspecting model outputs, we further observe that sampling produces more diverse tactics, ex- ploring various search paths, and is particularly effective in discovering number combinations.
Expert Iteration Figure 5 demonstrates the model performances by expert iterations. Gener- ated samples in TRIGO-gen usually have multi- ple proof paths, thus we apply the expert itera- tion (Polu et al., 2023) discover diverse and bet- ter proof paths. Specifically, we train the GPT-21- PACT model on TG-i, where i E [1, Then we employ the trained models to prove the training set samples in TG-i. If the proof pass, we add the new proof to the original TG-i. Eventually, we expand the original set to new training set Ii, where I indicates the 1st iteration. We retrain the GPT-21- PACT on TG generate new proofs, add the new proofs TG and obtain TG2-i. We repeat the above process times, obtaining TG' to TG We train the model on the seven datasets and evalu- ate them on the original test set of TG-i. As shown in Figure 5, the model's pass rate improves signif- icantly across all three TRIGO-gen datasets, with the largest improvement of 10.9% in TG-2. This highlights the diversity of proof path in training data for enhancing model performance.
We then explore the effect of increasing sam- pling temperatures. With temperature of 1.5, the model generates many illegal characters but outputs more diverse tactics. Reducing the temperature to 1.25 significantly decreases illegal characters, im- proving the model's pass rate on TRIGO-real, TG-1, and TG-2. These results suggest future direction of developing decoding methods to generate di- verse and valid tactics.
To compare different search algorithms, we lastly implement breadth-first search (BFS) and Monte Carlo tree search (MCTS) in previous work (Silver et al., 2017). Surprisingly, MCTS does not excel on our dataset. In Table 9, MCTS per-
Large Angle Values Evaluation To evaluate the model's
(OOD) generalization

---

Shen- Manual Labeling
TRiGO-gen
versity of tactics and search paths have significant impacts on the final proof pass rate.
Search Method
TRIGO-web TRIGO-real
TG-1
TG-2
TG-3
MCTS
32.55
24.06
$1.59
11.49
5.89
BFS
32.55
25.60
77.29
44.19
18,99
8 Ethics Statement
Table 9: Pass rate different search methods.
The trigonometric expression reduction dataset TRIGO is obtained from the Internet. After we col- lect the data, we formalize it in Lean and submit it to Lean to verify the correctness of the proof, without any bias involved.
Pass rate of diccerent expert iteration stops
80
TG-1
TG-2
70
When annotating TRIGO-real, we utilize not only the publicly available answers from "tiku", but also compose some the answers ourselves. As for collecting unlabeled data for TRIGO-web, we make efforts to gather solutions from diverse sources, encompassing blogs, documentation, Q&A com- munities, and even videos.
P055 RMC
50
40-
Eeration
Figure 5: The accuracy of the GPT-22-PACT model on the test set during expert iteration.
Limitations
Our evaluation metric focuses solely on verifying the correctness of the model's proofs. We consider the "no goals" output in the interactive environ- ment Lean-Gym as indication of success. Hence, this indicator serves as our metric for assessing the model's performance. In our future work, we aim to introduce improved evaluation metrics to assess the model's s ability to generate wider range of proof paths.
ability on numerical reasoning, we expand the range of angle values C' that can be sampled during generation to more complex set G {2TT, IT 32
3.- -I, -2 4' 5 7 8: 4. 5. 7: 8. g). and extend the maximum value of K from 100 to 1000. We
π
x
generate harder test sets for T2-1/2/3 respectively. We find that all models including the strongest baseline GPT-2,- model achieve pass rate of on these OOD test sets, revealing the limitation of current language models on the numerical reasoning.
Due to regional constraints, we cannot access the services offered by OpenAI, such as GPT-4 and GPT-3.5. Therefore, the evaluation of GPT-4 and GPT-3.5 our paper has been entrusted to researchers from research institution outside the restricted region of OpenAI, who conducted the assessment for this part.
7 Conclusion
this paper, we introduce TRIGO, a dataset focus- ing on trigonometric expression reduction for for- mal mathematical reasoning with both real-world and generated samples. To the best of our knowl- edge, TRIGO is the first Lean-based dataset with manually annotated and automatically generated reduction proofs for exploring the formal mathe- matical ability of current language models.
10 Acknowledgements
This work was supported in part by National Key R&D Program of China under Grant No. 2020AAA0109700, NSFC Grant No. 62276002, NSFC Grant No. 66.62006 Guangdong Outstand- ing Youth Fund (Grant No. 0021B151502006 NSFC Mobility Grant Award under Grant No. M- 0461, Shenzhen Science and Technology Program (Grant No. RCYX202007141 141 zhen Science and Technology Program (Grant No. GJHZ20220913
Our comprehensive experiments reveal that, in comparison to generated data, pre-training on PACT significantly enhances performance on real- world problems. Furthermore, expanding the data scale by utilizing real-world data the starting point for the theorem generation program can ef- fectively boost the model's performance on the real- world test set. Additionally, we reveal the model's incapability on generalizing numeric operations to larger unseen numbers and find that both the di-
Nansha Key RD Pro- gram under Grant No.2022ZD014 and Sun Yatsen University under Grant No. 221gqb38 and 76160- 1222001 1. We thank MindSpore for the partial sup- port of this work.

---

References
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. 2021. Isarstep: a benchmark for high-level mathe- matical reasoning. In ICLR.
Bruce Abramson and Richard Korf. 1987. A model of two-player evaluation functions. In AAAI, pages 90-94.
Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng. Yichun Yin, Lin Li, et al. 2023. Fimo: A chal- lenge formal dataset for automated theorem proving. arXiv preprint
Kshitij Bansal, Sarah Loos. Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019a. HOList: An environment for machine learning of higher order logic theorem proving. In ICML, pages 454-463. PMLR.
Pan Lu, Ran Gong, Shibiao Jiang, Liang Qiu, Siyuan Huang, Xiaodan Liang, and Song-Chun Zhu. 2021. Inter-GPS: Interpretable geometry problem solving with formal language and symbolic reasoning. In ACL, pages 6774-6786.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. 2019b. Learning to reason in large theories without imitation. arXiv preprint arXiv:7905. 10501.
Yoshua Bengio. Réjean Ducharme, and Pascal Vin- cent. 2000. A neural probabilistic language model. NeurlPS, pages 9338.
Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang. et al. 2023. Self-refine: Iterative refinement with self-feedback. arXiv preprint arXiv:2303.17661.
Karl Cobbe, Vineet Kosaraju. Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. 2021. Training verifiers to solve math word problems. arXiv preprint arXiv:21 10. 14168.
mathlib. 2020. The lean mathematical library. In Pro- ceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381. ACM.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In ICAD, pages 378-388.
Norman Megill and David Wheeler. 2019. Metamath: computer language for mathematical proofs. Lulu, com.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. 2021. Proof artifact co- training for theorem proving with language models. In ICLR.
OpenAL. 2023. GPT-4 technical report. arXiv preprint a/Xiv:2303.08774
Arkil Patel, Satwik Bhattamishra, and Navin Goyal. 2021. Are NLP models really able solve simple math word problems? ACL, pages 2080- 2094.
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the MATH dataset. In NeurIPS.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Man- tas Baksys, Igor Babuschkin, and Ilya Sutskever. 2023. Formal mathematics statement curriculum learning. In ICLR.
Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóždž, Piotr Miloš, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding hammers to integrate language models and automated theorem provers. NewrlPS, 35:8360- 8373.
Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03395
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, llya Sutskever, et al. 2019. Language models are unsupervised multitask learners. OpenAl blog, page
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In ICLR.
David Saxton, Edward Grefensteue, Felix Hill, and Pushmeet Kohli. 2019. Analysing mathematical rea- soning abilities of neural models. In ICLR.
Diederik P. Kingma and Jimmy Ba. 2015. Adam: A method for stochastic optimization. In ICLR.
Rik
Subhro Roy, Aida Amini, Nate Kushman, and Hannaneh Hajishirzi. 2016. MAWPS: math word problem repository. ACL, pages 1152-1157.
Jianhao Shen, Yichun Yin, Lin Li, Lifeng Shang, Xin Jiang. Ming Zhang, and Qun Liu. 2021. Generate & rank: A multi-task framework for math word prob- lems. In Findings of EMNLP, pages 2269-2279,
Guillaume Lample. Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. In NeurlPS, pages 26337-26349.
David Silver, Julian Schritwieser, Karen Simonyan. Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, 2017. Mastering the game without human knowledge. nature, 550(7666):354-339,

---

Yan Wang, Xiaojiang Liu, and Shuming Shi. 2017. Deep neural solver for math word problems. In EMNLP, pages 845-854.
Kumhao Zheng, Jesse Michael Han, and Stanislas Polu, 2022. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR.
Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hanna Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in nat- ural language. In NeurIPS.
Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, and Roger Baker Grosse. 2021a. INT: an inequality benchmark for evaluating generalization in theorem proving. In ICLR.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large lan- guage models. NeurlPS, pages 32353-32363
Yuhuai Wu, Markus N. Rabe, Wenda Li, Jimmy Ba, Roger B. Grosse, and Christian Szegedy. 2021b. LIME: learning inductive bias for primitives of math- ematical reasoning. In ICML, pages 11251-11263
Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, al. 2023. Lego- prover: Neural theorem proving with growing braries. arXiv preprint arXiv:2310.00656.
Jing Xiong, Chengming Li, Min Yang, Xiping Hu, and Bin Hu. 2022. Expression syntax information bot- tleneck for math word problems. In SIGIR, pages 2166-2171.
Jiong Xiong, Zixuan Li, Chuanyang Zheng, Zhijiang Guo, Yichun Yin. Enze Xie, Zhicheng Yang, Qingx- ing Cao, Haiming Wang, Xiongwei Han, Jing Tang, Chengming Li,
Xiaodan Liang. 2023. Dq- lore: Dual queries with low rank approximation re-ranking for in-context learning. arXiv preprint arXiv:2310.02954
Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In ICML, pages 6984-6994.
Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chala- mala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmenned language models. arXiv preprint arXiv:2306.15026.
Longhui Yu. Weisen Jiang, Han Shi, Jincheng Yu. Zhengying Liu, Yu Zhang, James T Kwok, Zhen- guo Li, Adrian Weller, and Weiyang Liu. 2023.
Metamath: Bootstrap your own mathematical ques- tions for large language models. arXiv preprint arXiv:2309. 120.8244...1..
Chuanyang Zheng, Haiming Wang, Enze Xie. Zhengy- ing Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. 2023. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint 23099 15806.

---

A Implementation Details.
We employ identical hyperparameters to train GPT models on both the PACT and TRIGO datasets. The Adam optimizer (Kingma and Ba, 2015) is utilized with a learning rate of 2.5 x 10 and a cosine schedule, while the batch size is set 512. During training on TRIGO, we a maximum epoch limit of 20 and select the epoch that achieves the lowest validation set loss. For PACT training, we conduct an initial pre-training epoch on the mathlib, mix I, and mix2 datasets provided by PACT. During the proof search phase, beam search is applied to gener- ate tactics with beam size of 16, and we consider the top 8 outputs. Additionally, a maximum budget of 512 search steps is allotted. All experiments executed on 8 Nvidia Tesla V100 GPUs.
NE,.1 1+ C(o. ' (2)
(UCT(,, Q + Po(t
t" arg max PUCT(g, ICA
where (g, t) denotes the value function of sam- pling tactic t in proof state A denotes all the tactics that can be sampled, Po g) denotes the prior probability, and C(g. t) denotes the number of visit counts of the sampled tactic t in state g. In our experiments,
always set the constant e 1, and we use the cumulative probability of the model output tactic as the value of Q(g, t).
D Informal Mathematies Benchmarks
In contrast to formal benchmarks, informal bench- marks lack data annotated in formal theorem proving language. Constructing formal mathemat- ics time-consuming and demands a high level of mathematical expertise from contributors. In- formal math problem datasets, represented in nat- ural language, are more convenient to construct. Math word problems KKoncll-eezziors 2016; Wang et al.. 2017: Patel et al., 2021; Cobbe et al., 2021; Xiong et al., 2022, 2023; Yu et al., 2023) target elementary students, querying an un- known variable given a natural language situation description. MATH (Hendrycks et al., 2021) )) con- tains 12,500 high school math competition prob- lems with natural language statements and solu- tions. These datasets, collected from real human problem-solving. better reflect real distribution but lack strict formal verification to ensure correct- ness. NaturalProofs (Welleck et al., 2021) uses nat- ural language to describe mathematical statements and proofs, while (Saxton et al., 2019) syntheti- cally generates lems represented as pure strings, covering various topics. However, due to natural language ambigu- ity, the correctness of the proof process in these works cannot be verified.
B
Case Study
We provide an example of the model's search on TG-1 in this section. As shown Figure 8, this example demonstrates a correct proof step, and we can see that the model employs the tactic of "have" to make multiple assumptions, However, often the goal of many hypotheses to prove is trivial, so deter- mining how make useful assumptions is crucial factor in the model's proof accuracy. Furthermore, the model's s ability to combine the numbers in the "have" tactic also determines whether the model can reach the correct proof path.
et al.,
As shown in Figure 9, this example demonstrates a proof step where the model fails. The model ap- pears struggle to output diverse hypotheses to explore more proof paths when forming a search tree but generates a large number of identical "have" tactics. It highlights the importance of using a vari- ety of exploration strategies to improve accuracy.
math prob-
As shown in Table 10, GPT-4 with the In-context learning approach performs well in both the second and third examples, while methods using natural language instructions fail completely. These exam- ples illustrate that GPT-4 is capable of learning the compositional relationships in numbers through in-context learning in one-step proofs.
E Neural Theorem Proving
DeepHOL (Bansal et al., 2019b) first applies rein- forcement learning to automatic theorem proving without human- -writtn proofs, achieving the best performance on HOList. AStactic (Yang and Deng. 2019) treats tactics as programs and composes ab- stract syntax trees (ASTs) during tactic generation. LIME (Wu et al., 2021b) introduces inductive bias
Experimental Details of Monte Carlo Tree Search
We provide here the details of our implementation Monte Carlo Tree Search. We follow the formula below to generate each tactic t":

---

In CoNTET
GOAL (c0s(150/p//3) cos (13111/p)) PROCESTED have: cos(pi/3) (cos(155pp//3),
GOAL - sin si cos (pi / 3) cos si sin (5 + pi 31 / sin pi 31 /
COAL 10 tan (66 ppl A api scos /ptipt/3:
PROOFSTER have: 2aain(p1) cooppppoalpppaaea......o
aasintp:/soon / /3//3/oo
tar 165 pij tan (187 pl
PROOESTER have: tent-pi/2 = con(66)p)),
GOAL cos
pi 2:
pil PROOFSTED have: sin(pi) cos(E9xpi/21,
GOAL ED : ain (pi / 31 6, hi 1.2 sin ipi 3) * 3, 62 ain (2 pi 3) 12 ain (pt 31
9, h3 sin 12
#
sin (pi / 3) . 2 sin pi
FROOESTEP have: cinipt/3) (ttp/////o1n12221/3333
(2rsin(p1/3111 = 2scinipt/31 wtt./////22///222///2//
COAL this : cos (pi
22- 0oa (31 12) 1-22-1 sin ((-2) pp
sin (-pi / 2) cos (şi /1// 61 sin (pi / 6: coB 1-pi / /
PROOFSTED
sint-2rgi/3)
sin(-pi/21
coa(pi/6] ain(pi/61 (-s(-p//21,
GOAL coa (-p1) = sin ((-133) + p- / PROOPSTEP have: -sin[[-133) + p1 2) sin(-133+p5/2),
GOAL -iin ((-) pil (-2)
((-2)
sin 1293 pi 21
PROOFSTEP have: (pp) -sin(299.p1/2) 2usln(22shh
GOAL
GOAL : (29550901//) # C, this tant pi/3)
sin(drp1/3) (poz))
H cos (333///3))
(inipi/3)-o scos
(pi/6)+++
(-1)/tan (29bpp//6)
2x1/2 (psa1
PROCESTEP
sin(-pi/31 //c////ccc//p//////
PROOPSTE2
Landt pi/3; PROOPSTEP
GPT-4
have: con (2ep1/3)
bave: sipptpp//) (aallppp/3///o//aee (-p/33
have: (4p/1/) (p1/33
2+cos (pt/tpp//111 +12
(-n(-3)/3),
sin -co: (1ps53333333
Zasinip' /2) xo0s (pi/21,
Instructions
expest lean. Now will give you
You expert Lean.
You
expert in will give you a one step
Now
Now I will give you a
step goal proof pair:
peir:
geal proof pais: 60AL F
COAL -ona (154+p1/3)
COAL "0 54+p1/3)
ona (154+p1/31 cos (131.p//3)
cos (c:(131p// PROOFSTEP cos (pi/3)
cos (131.pi/3) PROOFSTEP have:
PROOFSTEP have: cos (ps/3))
cos (pi/3)
(354xp1/3),
cos 34xxp//)), Please
-coa (154xp1/31, Ploase provide tactic that includes She word "have"
Please provide a tactic that includes the word "have" as shown the example above: GOAL ho can (455 this can (-pi/313))-1 (-1)))1---11001))1) /tan (295
provide a tactic that includes
the word "aave" show
the exarple ahoves COAL
shown in the example abeve: GOAL oos (433
(4.p133)3)) scos tpl/3/
sin (co0ppp1//
pi / 3) - 2 zos (pi / 6)
24sin (p scos (pi/2) PROOFSTEP
PROOFSTED
E ain /ooa (-pi/31
can (-p1/3) PROCESTEP
GPT-4
PROOFSTEP have: (433xp1/3) (433
PROOFSTEP have: tan tan/3i/3 (113.p////)))
PROOFSTEP have: sinl2spi) -
sir11-21 xpf)
med 6) xp1/3)
GT
have: cos (p1/3) cos (433-pp1))
have: sin cinl-ps/3//cos111pe can
have: sin(pi)
Table 10: One-step proof' from 8-shot in-context demonstrations generated by GPT-4. We compare results from in-context demonstrations and natural language instructions.
of reasoning into language models through syn- thetic tasks. GPT-f (Polu and Sutskever, 2020) is the first work leveraging pre-trained language models for automatic theorem proving, generating tactics, and proposing proof search expansion for
language models, allowing them to generate novel skills and enhance success rates in mathematical theorem proving tasks, thereby paving the way for new avenues in the theorem proving community.
F More Details on Automatic Sample Generation
efficient proof tree searching. Our experiments pri- marily reference GPT-f's design. PACT (Han et al., 2021) extends this line of work through co-traine co-training generating models with multiple self-supervised auxiliary tasks, providing the strongest baseline model after training on PACT's pre-training corpus. Lample et al. (2022) extends MCTS (Abramson and Korf, 1987) hypertrees, proposing Hyper- Tree Proof Search for theorem proving. Polu et al. (2023) explores curriculum learning for perfor- mance improvement, which we incorporate through expert iterations in our study. Xin et al. (2023) ex- plores the utilization of a growing skill library to augment the theorem proving capabilities of large
As illustrated in Algorithm 1, we have devised our automated sample generation program by draw- ing inspiration from the manual annotation pro- cess of problem-solving, as depicted in Figure 7. Lean- Gym implements a strict replacement strat- egy and does not perform reduction operations like sympy. Specifically, when performing the expres- sion replacement step, since we use sympy to parse the expression tree, it automatically reduces the expression to the new equation eqt, causing mis- alignment with the equation eqiean in Lean's 's proof goal. To solve this problem, we use the "have" tac-

---

Types of tacties
TRIGo real
TG-1
TG-2
TG-3
Temit-ral
TG-1
TG-2
TG-s
Problem
Taetic
Problem
Thetic
Tictic
all metics
10,574
209,662
349,393
498,417
have
2,179
32,490
53,955
Train
209
7,338
9,000
115,475
189,138
274,373
Val
42
1,212
1,000
13,819
22,220
31,660
Ratio
0.206
0.155
0.154
0.153
Test
86
2,024
1,000
14,285
22,979
32,021
427
10,574
11,000
143,579
234,33
338,054
Table 11: Statistics for Ratio of "have" tactic
Table 13: Statistics for TRIGO-real.
TRIGO-real
TG-1
TG-2
TG-3
dag
H General Tactic
37
22
35
49
81
In this section, we present several tactics we gener- ated along with their corresponding annotations Table 14 shows several typical tactics, such as "field_ fheld_simp", both of which are high-level tactics that can handle many expressions involving field operations such addition, multiplication, and in- verse. We do not consider "tidy" when generating the data because this tactic is easily timed out.
Table 12: Average number of tactics per dataset.
tie for alignment, for example: "have Clean try field simp at &, try repeat left, tryring, conv to to__hh lhs, rw this", where Clean and Cp respectively represent the side of the equation eQtean and eq; that is to be replaced. These tactics automatically align the proof target in Lean's proof goal to egt- We present generation algorithm in Algorithm The algo- rithm continuously iterates in the forward process, randomly sampling rules and parameters gener- ate problems at each iteration, and interacts with Lean-Gym to ensure correctness. Once the speci- fied number of replacement rules or the maximum number of iterations is reached, the algorithm stops and collects tactics in reverse to obtain training data.
I Rule Specifications
In this section, we present all the rules manually defined in Table 15-17. For each rule, we create corresponding tactics to ensure that the proof of the problem can be collected backward after generating the corresponding tactics forward. We demonstrate the mapping of some rules their corresponding tactics in Table 38. During the complete process of annotating these missing reduction steps, as demon- strated in Figure 7, we illustrate how it is matched with the rule specifications, undergoes a one-step transformation, and results in a new problem state.
G Dataset Statistics
In this section, we present the average proof length for TRIGO, along with the split of the training, val- idation, and test sets TRIGO-real. We show the proportion of different tactics in Figure 6. Addi- tionally, we display the proportion of occurrences containing the "have" tactic shows the average lengths of the datasets in TRIGO. Table 13 shows split TRIGO-real.
Annotator Demographics
Our annotation team consists of four Master's stu- dents and three PhD students. The Master's stu- dents are responsible for completing the annotation of informal proof steps, while the Ph.D students fo- cuse on formalizing the informal proofs into Lean. The four Master's ' students holds a Master's degree in Computer Science. They have received rigorous mathematical training and possess in-depth knowl- edge in the process of reducing trigonometric ex- pressions. The three Ph.D students are in the field of computer science specializing in formal theorem proving. Four Master's students firstly simplify the trigonometric functions, then Ph.D students man- ually translate these informal proofs to Lean and submit them to the Lean theorem prover for cor- rectness checking. The combined process of data annotation and mathematical formalization took one month complete. The personnel involved in
in Table 11. Table 12
We can observe that TG-2 has the closest average length to the TG-real. From Table 11, the propor- tion of occurrences containing the "have" tactic in TG-2 is smaller than that in TRIGO-real. Although the average proof length is different in TRIGO-gen, the occurrence of the "have" tactic is roughly the same. Additionally, upon closer examination of the data, we find that the "have" tactics in TG-3 is comparable in complexity the "have" tactic in some of the data in TRIGO-real. The aforemen- tioned statistical data reflects the disparity between the distribution of generated data and real-wor world
data.

---

others
SocuR
focus
24.5%
11.8%
simp
simp
7.0%
10.25
13.158
17.0%
16.9%
TW
ring
(a) TG-1
(b) TG-2
others
others
have
24.2%
linarkh
6.2%
5.5% 37.
6,3%
filld
repeat
19.4%
14.4%
10 0%
apply
20.0%
ring
(c)
TG-3
(d) TRIGO-real
Figure 6: Tactic distribution of TG-1, TG-2, TG-3, TRIGO-real
the formalization work are also co-authors of our work.
techniques of grouping and factoring in trigonomet- ric reduction.
We conduct numerous zero-shot tests on our dataset using GPT-3.5 and GPT-4, employing the prompt "Please
K
Data Example
prompt"Please help me prove the following lemma
We show examples from our dataset in this section. Table tables 18 to 25 shows typical examples in TRIGO. This data can be compiled correctly within Lean-Gym, and after compilation, interact with Lean-Gym obtain the final training data.
using Lean: lemma Trigo_ 0 [PROBLEM] ==. However, we find that GPT-4 tends to output a lot of meaningless tactics, such as the case shown in Table 35. Moreover, GPT-4 often generates tactics that do not exist in the dependencies, seen in 35. The example in Table 35 reveals that GPT-4 is prone to making trivial assumptions. By comparing the output of GPT-3.5 and GPT-4 tables 34 to 37, we observe that GPT-4 is more inclined to generate "have" tactics, which is closer to the proof pattern of our dataset.
L Large Language Model test examples
In this section, we demonstrate examples of in- context learning and zero-shot methods on large language models. In contrast the single-step proof context learning in Table 6, the examples of context learning presented this section di- rectly provide the entire proof. We find that it is challenging for the model to provide correct proof. Tables 30, 32, 26, and 28 show examples of our in-context learning approach tested on our dataset using GPT-3.5 and GPT-4 models. Tables 31, 33, 27, and 29 show the outputs of these models. We find that LLMs have difficulty learning to use the correct "have" tactic, which suggests that LLMS may not be able to manipulate numbers and lack gemeralization abilities such as the commonly used
The experiments above all indicate the limita- tions of LLMs on our dataset. We leave to future work on how to enable large language models acquire complex number combinations ability and reduce illusions.

---

Tactic
Function
field_simy
The goal of field_siin sii__impp_ is to reduce an expression in field to an pression of the form where neither nor contains any division symbol.
simp
In Lean, simp a tactic that stands for "simplification. It is used to sim- plify expressions and goals by applying set of predefined rewrite rules and simplification procedures. The purpose of simp is to automatically transform complex or convoluted expressions into simpler forms, making them casier to work with and reason about.
rip
A factic for solving equations in commutative (semi)rings, where the exponents can also contain variables.
ring
Evaluate expressions in the language of commutative (semi)rings.
assumption
The assumption tactic looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.
repeat assumption
The repeat assumption tactic looks through the assumptions in context of all goals, and if the assumption of the context of the current goal can match the target, then it is applied.
left
The tactic tries to solve the left disjunct immediately by assumption; if that fails, it tries to focus on the right disjunct; and if that doesn't 'tt work, it invokes the assumption tactic.
refl
In the proof language Lean, refl is an abbreviation for "reflexivity." is used as a tactic to automatically prove goals of the form a, where is any term or expression. Essentially, asserts that any term is equal to itself, which is a fundamental property of equality.
have
In Lean, "have" is a keyword used in proof scripts to introduce a new intermediate goal or hypothesis. It allows the user to assert a proposition and then prove it separately before continuing with the rest of the proof. In Lean, conv is tactic that allows users to perform step-by-step rewrit- ing and manipulation of expressions within proof. stands for "conver- sion" " and provides flcxible way to apply various rewrite rules, simplify expressions, and rearrange terms.
conv
to to_lhs
The lo_hss modifier is typically used within a tactic block, such as conv or rewrite, to specify the side of the equation or expression that should be modified. When to Ihs is used, the tactic will focus the LHS of the equation or expression and perform the specified operations on that side. In Lean, rw is a tactic that stands for "rewrite". is used to apply a specific rewrite rule to an expression or goal within a proof. The rw tactic is commonly used to replace occurrences of a specified term or pattern with a different term or pattern according to given equality.
rw
apply
In Lean, the apply tactic is used to apply a theorem or hypothesis as rule to prove goal or generate new subgoals. It allows the user to an existing proposition to infer or establish other propositions.
congr_arg
In Lean, congr_arg is a function that allows users to apply congruence to a function applied to an argument. is used to prove equalities by reasoning about the effects of a function on its arguments.
Table 14: Examples general tactic.

---

Identity Rule Name
Example
sin zero
sin (0)
sin_pi
sin (T) = 0
ti__ttt_pi_dd__heeeeeeeee three
sin (
(x
V3
3
2
sin wwwttteeeee_diii___e four
sin (3r)
4
V22
sin five dive_pi_dii_ si_div_sit six
sin (5x)
6
2
sin_pi di_ twelve
sin T
12)
V2
4
+
vB
sin pi_ppp___ did_vi__oo
sin (Ø) = 1
sii_pi____________pppiiss div dl__divtthere three
sin (3) y3
sin div four
sin (4) v/
sin sin_pi__di__st
sin (g)
cos_zero
cos (0) =
cos cos_two_pi__dt _iv_iiiiiiiiie_eeeee tir__e
cos (2m)
2
cos_ cos_three_pi_ pirree_p_ddi___e piur four
cos (3x
(4)
//2
cos cos_ fiveev_pi fos_five_pi_div_tl
cos (gg
v/3
cos_pi
cos (x) = -1
cos_pi cos_pi_div_twelve
cos (22 =
V2
+ V6
4
cos_pi_div_twa two
cos (ï) 0
cos pi div three
cos (5)
1
2
cos_ cos_pi_div pi_ four
cos (H)
x/2
2
cos jos_pi_div__ae six
cos (T)
/3
2
tan_zero
tan (0) = 0
tan_pi
tan (IT) = 0
tan cin_tto__pi_deee div three
tan (2 - 33
tan three _i__ii__iv diy four
tan 1
tan ttn_pi__a______ div twelve
tan 4
2 - V3
T2
tan Lan_pi_at____ppp pii_pi_dv____teee three
Lan [5] = v
tan tan__i________ pid_iiddvv__repee dour
tan [ = 1
tan han_pi_div_ss
tan [)] v/3
Table 15: Examples of identities in our pre-defined rule bank. Notations (1/3).

---

Identity Rule Name
Example
sin neg
sin (X) = sin (2 x π * K - X)
cos nog_
cos (X) = cos (2 x + K - X)
tan_neg
(TT * K X) tan (X) tan
sin_ add_inntd_ad__ _a____nt_________ _t
sin (X) sin (2 * K + XX)
cos cos_add Lind_iit_uuuit ant__mul_ttop
cos (X) cos (2 π * K + X)
sin_add sin_add_int_mul laammmltt_pi_atteee pwo_pi_add_ii sin (X) = sin (X + π (2 + K + 1))
_os_add_int_mul__e _ww_tto_pi__dd_______aa__ap
cos (X) = COs (X + π * (2 * K + 1))
con_add_int_min
tan (X) tan (T K X)
sin_neg_add pog__addintt___ ios__int__uu____ two _to__tt__d______________________ sin (X) sin (-X (2 K + 1))
cos_neg_add_ing aai__ddd_it__mn int_mull muul_tww___.._ _eto_pp__dd__pp__p_ee cos (X) = cos
π * (2* + 1)) X + (-X
sin_ sin_add pi pi_div__twe
sin (X) = cos
(2 * r * K + X 3)
sin add pi pi_div tww swo_add_pt
sin (X) = cos (X + π * (2 + K + 1) + +)
sin_neg_wwl add pi_ div ttw __ddadd_pp
sin (X) cos (-X + + (2 K 1) 1) + +
cos_add _i__dddpi_diii pi_div__dd_ two
cos (X) sin (2 π K X +
pss_addpi_diiv_wee __dd__dd_ppi
cos (X) = sin (X + π * * K + + +
jos_neg_aadd_ii_dl_ttoooaae
cos (X) = sin (-x + π (2 * + +)+ 5
ian_add_pi__ts two
tan (X) tan( [To +
sin_neg__at add _eeg_add_p___eeeeedeeeee___ee_ _ip_pidiii dwo
sin (X) cos (2 π K - X
cos _i__e___dddpi_dii__ee
cos (X) = sin (2 π K X +
tan tan_neg_add wwa_eee__dd___eeeec ai__adddpp_dv_vwe____ dwo
tan (X) tan ToK x +
tin_two_mm _wl_
sin (2 X) * sin (X) * cos (X)
sin tettttere__mm mul
sin (3 X) -4 sin' (X) + 3 + sin (X)
cos cos_two_mul
cos (2 X) 2 * cos? (X)
cos vos_two_mul_2
cos
(2 X) = sin? (X) + cos? (X)
cos_two_mul, _
cos (2 X) = 1 - 2 * sin² (X)
cos cos_ cos_three_mml
cos (3 X) 1 * cos (X) 3 * cos (X)
tan_two_miu
tan (2 X)
2*tan(X) 1-tan (X)
[os_ss_cos_two__
sin (x)²
1-crs(2xX)
2
cos (X)² (+xx)
cos_sq_cos_two_mmg
sin(2+X)
cos_eq_sin_two_mes mul
cos (X) 2=sin(
sin mo__e__inn_tt____ mul
sin (X)
sin sin(2+X)
2+cos (X()
Table 16: Examples of identities in our pre-defined rule bank. Notations (2/3).

---

Identity Rule Name
Example
sin_add sin
sin
sin (X) + sin (Y) - 2 sin (x+Y)
* cos
(zz²)
sin_sub_sin
sin (X) sin (Y) - 2 sin (x_Y)
* cos
2
cos_add_cos
cos (X) + cos (Y) = 2 cos (x²²) * cos (xtrr
cos_sub_cos
cos (X) cos (Y)
sin {>) Y sin (x+)r
tan_ han_add_tan
tan (X) + tan (Y) = (1 tan (X) * tan (Y)) * tan (X + Y)
tan_sub_taa
tan (X) tan (Y) = (1 + tan (X) * tan (V)) * tan (X - Y)
tan (X) tan (Y) sin(X-1)
tan lan_subb____ s_b_tuutt_______ 2
tan div two_]
tan (X/2) sin(X)
Xx)
tan tan_div__ta _iw________
tan (X/2) 1 (X)
sXn(()
sin_miu Sin_mul_sin
sin (X) * sin (Y) = cos(X n cos(X+N)
2
sin (X) cos (Y) sin(X++)+sin(X--
sin jin_mu_coos
2
cos ss__mu__in
sin (Y) * cos (X) sin(X+t)-sin(X*
cos (X) cos (Y) cos(X-))) -coxx
cos_muu mos
2
tan (X) * tan (Y) tan(X) tan(Y)
tan tan_mul_mm ____mu__tnn -an
tan(X-Y)
tan (X) * tan (1) tan(X) (ta(()
can_mul_tan
+
tan(X+Y)
sin_add
sin (X Y) = sin (X) * cos (Y) + sin (Y) cos (X)
sin_sub
sin (X Y) sin (X) * cos (Y) sin (Y) cos (X)
cos add
cos (X + Y) sin (X) sin (Y) + cos (X) * cos (Y)
cos cos_sub sub
cos (X - Y) = sin (X) * sin (Y) + cos (X) * cos (Y)
lan_add
tan (X + y) = [an(X)+tamm
T-lan X [P]
tan_sub
tan (X - Y)-
I+tan [X)+ta][]]
Lan(X) -tan(y) (Y)
tan
tan (X) cosiX)
sin(X)
sin_ gon_div_cos_ee_taa _an
sin(X) (Xs
tan (X)
sin_sq_add_cos_ss
sin² 2 (X) + cos? (X) =
sin_sq
sin 2 (X) cos22 (X)
cos_sq sq
cos? (X) 1 - sin2 (X)
Table 17; Examples of identities in our pre-defined rule bank. Notations (3/3).

---

Trigonometry Simpifficaiin Annotator
Deghy
-oottrtyyy (--40/100) MaOCCMAAY moy suaas
at
Soees
Dedern e9/01/0 aetorzze
GRal Jram p romid train
Exposiaa
Digpht acprassu
Da:
(a)
(b)
Figure 7: The interactive annotation system for trigonometry reduction, (a) interface our system. Region shows the problem to be annotated. Region @ is the main interaction area where annotators imput equation for the current step. The system then matches with the rule bank, performs a one-step transformation, and outputs a new problem state. Region @ shows the annotation history and region includes interactive buttons for annotators to change reset the problem, check examples, and trigonometry knowledge to help their annotation. (b) The workflow our annotation system.
state: -110(330p////11//
have (in(51p1/6) ((1tg358t1/8s)
have caagpt/66---tt((55pp0))))
state: goals
stn(s"pt/6) -sle(35tp1/9) stn(SPp(/4) -$in(35'pp16) -Sin(55'pt/6) 1/2
Error
re sin.wu rug aini int, si (3/s1/6) (2),
rsled_ster,
na sin PoL sin int_ Ivo, si (5tp4/0) (5),
Proof Path
Error Path
Error
focpeatepeat (apply congr_arg _}b, simp,
ring, conv (to 1hs, this,), have
sin(5"pi/6) 1/2,
sin__iive_i_diii pi___i______.p_-_iiiiipppp__
goals accomplished /
Search
Figure 8: Case 1. The light yellow dotted line indicates the remaining steps. Due to page constraints, we do not draw the entire proof tree.
steps.

---

state: cos (-pi) cos pi (-2) (-sin (-pi 3) cos ((-4) + pi/
((-4) / 3) cos (-pi sin
have (-2) * sin(O) (sin((-4) pi 3) cas(- sin(-pi/ / 3) cos((-4) pi 3))
--2(--ii(--pill (00(-pp///ooosss 4xpi/3) sin(-4 4-pi/3)rccs(/ pi/3)))sin(O).
1906 Taok
1it caso mind-l 28 canroi 2- 1a contleteel 18
siepd_simp at
Paee calet wa ra por di drtirper www.
conv (to_rhs,
rhs, rw this,).
sin(- (4n-4)-i/3) cos(-pi/3)- pi//)pp/3)--- cos(-4rpi/3), have : sin(-pi) sin((-4-pi/3) (-pi/3)),
apply congr_arg, ring.
search failed
rw this,
ring.
conv (to, rhs, this.). have cos(-pi) pi) cos(pi) 2 sin(0) sin(-pi),
Search
Figure 9: Case 2. The light yellow dotted line indicates the remaining proof steps. Due to page constraints, we do not draw the entire proof tree.

---

Algorithm 1 Theorem Generator
I: function GENERATE, THEOREM(len of step L., rule list R.
2: Randomly select rule from R.ro Unaform(R).
3: Initialize the parameters X, Y, K in ro and get its initialization state in lean and expression:
Pstate: eqo + INITIALIZE( (ro).
4: Init TactiCproves Peount: 0,0 <- INIT()
5: for - to 200 do
6: Randomly select rule from R.R,y ~ Uni)
7: Match the formula Rj on the left side of the R₂ equation with the formulas et and on the left and right sides of eq--1, and return the matching parameters. Since there are multi- ple matches, matching result can be randomly selected: Para: RULE_ MUTCCNNACCI ei). Para, < MOLL__MMTCHNNG R1, Cr)- Substitute the parameters into RŞ-
8:
9:
if Paray is not NULL then
10:
R1 f PARAMETER (R Parri)) Parai),
11:
R, f- PARAMETER (E Para:)
12:
else if Para, is not NULL then
13:
Ri <- PARAMETER PARAMETER_REPPLACEMEEE REPLACHMENT (Ri; Parar),
14:
R < PARAMETER BEEERR__EPAAAEEEEEEE R,, Para,),
15:
end if
Perform equation replacement operation: eq: EQUATION REPLACEMENT(eq 1, R, R.
Get the factics corresponding the rule: TacticsR, < Rg GET Ta R.,) Obtain the tactic of adjusting the cross terms in equ-11
18:
19:
Para is not NULL then
20:
T Tacticsterm <- GET_ SLRE__CROS_iiA TERM(a, R2), if Para, is not NULL.
21:
else if Para, is not NULL then Tacticsterm + GET_CROSS_ [eRnSs_TTRM(er Rp), elif Para, is not NULL.
22:
23:
end if
24:
Apply TacticsR, and Tacticsterms LEAN-GYM to obtain the GOAL in lean:
GOALieans ERROR SELL_TTATTCS(U) Tcclicssrrm T TaclicsR..
25:
if ERROR NULL then continue end if
26:
27:
28:
Align the proof goal equation eqtean in GOALlean with eqi: Tacticsatign CCROO_STERRA Apply Tacticsatign to lean: GOAL, ERROR <- OPPLY_TACTICS (aaeticssTactcsaaaaaa Tacticsatigll if ERROR is not NULL then continue
eq:).
29:
30:
31:
32:
end if
33:
Tacticprone &- TactiCproee Tacticsatign U Taclicsterm Tacticsn. Poount &- Poount +
34:
35:
if Powunt = L then
36:
break end if
37:
38:
end for
39:
return TactiCprove
end function

---

lemma Trigo_0_17_FTGL sin(-19xpi/8)=1/2;= begin have : sin(-19xpi/)) sin(-7*pi/8),
rw sin_ss_sin__dd__ii_mmt_www (-19+pi/6) (1),
repeat (apply congr_arg _ simp, linarith,
},
rw this, have : sin (-7+pi/6) sin
zw _dd_____________________________ in int_iinn_ttttt_ _ww__wo__pi_ii (-7xpi/6) (0),
int
repeat (apply congr_arg _), simp, linarith,
},
rw this, have : sin (7xpi/6) -sin(pi/6),
Iw ait. add (7xpi/6) (-1),
repeat (apply congr_arg _ simp, linarith,
), rw this, Iw sin_pi_div_six
norm_num, end
Table 18: Example of TRIGO-real

---

lemma Trigo KOPV
(h0 sin(11/18 2 0)
(h1 -cos (pi/18) sin(pi/18) < 0)
(h2 : -sinnp1//11))
cos (pa(1/1)) # 0)
sqrt (1 ccn(p//))//(oorrt
cos (17+pi//18)** ++2) cos (35xp1/18)) =1:
begin
Iw f sin_sq,
have sin(pi/9)
2*sin (pi/18) +oos (pi/18),
have : sin (pi/9) sin (pi/18)),
apply congr_arg, ring,
this, sin_twe_mul,
rw this, have 2 cos (m/18) (pi/18)) A-2 cos (pi/18) .22
2*sin 11)/18) coos (pi/18),
sin_sq_add cos_sq,
this,
have =x2 (pi/18) 2xsin(pi/18) ,cos (pi/18)
(-i0111)118) sin(pi/18))
eipg_exp,
this, (in(11+p//18) sin (p1/18),
have
Iw jen.e__eii_egggedd_ii..........
(17-pi/18) (0),
repeat lapply congr_arg _), simp,
linarith,
zw this, have cos (35+p1/18) cos /18),
rw joo__o__os_nog__o________ _tt___________p (35xp1/18) (1),
repeat (apply congr_arg _), simp,
linarith,
b
rw this,
repeat (rw sqrt_ sg eq abs),
Tw fosmeq_self.mpp ho, rw soo__oe_no_soof..gg hl, norm_num,
field_simp,
end
Table 19: Example of TRIGO-real

---

lemma Trigo_0 : sin (107+pp)))0:: begin
have cos (pi/2) sin si077pp))),
Iw cos_eg_sin_ add add__id_di__tto_eeeee___________ _adddddddddda_deeee int mul __ (pi/2) (53), focus ( (repeat (apply congr_arg _}} simp, ring,
}
conv [to_lhs, rw f this, ), have cos (pi/2) = 0,
IW cos pos_pi_dii civ
rw this,
end
Table 20: Example of TG-1
lemma Trigo_3 -sin (-pi/4) x*2 cos (-pi/4) **2 sin (51xpi) begin
have cos (-pi/2) -sin (-pi/4) cos c-si-p) 2, have : cos (-pi/2) cos (2* (-pi/4)),
apply congr_arg, ring,
),
Iw this,
cos_two_mul',
ring,
,,
conv [to_lhs, zw + this, ,
have : cos (-pi/2) = sin
intpaaaddmdaaaii...o..dddaimiimm int__iiit_______ (-pi/2) (25), focus(repeat: (apply congr_arg _ simp,
rw
ring,
},
rw this, end
Table 21: Example of TG-1

---

1emma Trigo_1 (h0:sin (1877p 0) (h1: (118)
0):
-sin (1187 (2+sin (1177 =sqrt ( 2 / 4 + sggrt ( 6 ) / 4:
begin
have (sin (1187 / (2xsin (1187ppp11))))) -sin
/ (2+sin (1187xpi/12)),
Field_simp at *,
conv [to_lhs, zw + this,
have : cos (1187xpi/12) = sin (1187.p1//)) / (2.5in
have sin p1187)p)/// (2+ (1187)p//12))
{
apply congr_arg, ring,
}
rw this,
rw sin_two_mul, field_simp at ring,
},
conv [to_lhs, rw this, ,, have : cos (pi/12) cos -os (1187+p1/12),
rw htg.aannggoooonnggo.a.a.taaaroar focus(reped) (apply congr_arg } simp, ring,
(pi/12) (49),
}
conv [to_lhs, rw this,), }, have cos (pi/12) sqrt (2) /4 sqrt (6) /4,
IW cos cos_ppi__pe__eeeeeeeeeeepeeeeeee div__tidiv_twelree
b,
rw this,
end
Table Example of TG-2

---

1emma Trigo_2 (h0 : cos (44pp//3)/2) 0) (h1 (cos (4xpi13)))) +1) 0)
(h2 :
(1+cos (4*pi/3)) 0) cos cos (-5xpi/66)) (cos (4+pi/3)+1)==qqp) (3) :=
begin
have : cos (-5) +pi / 6) / (cos (4+pi/3)+1) +1) = cos (-5xpp11/6) / (cos (4+pi/3)+ +1),
simp at ,,
have (4xpp/13 cos cos
rw ottpppoonnngaaaaoooooooooooooaaa setpo__dddintt__i___e (4xpi/3) (0),
freps(repeat: (apply congr_arg }
simp, ring,
} conv [to_lhs, rw this, have : (in(4/1/33) ( (1icos (4xp1/3)) sin (4vp1/3)) (40s(4)) 1)
field_simp at *, repeat (left), ring,
} conv [to_lhs, rw <- this, have : tan (2xpi/3) = sin(4xpi/3) / ( (4spp1))
have : tan (2+pi/3) tan (annpp333) /2),
apply congr_arg, ring,
},
rw this,
rw tan_div_two', repeat (assumption),
},
conv (to_lhs, rw this, },
have : tan (2xpi/3) sqrt ( 3 )
{
IW can_two_piicci__teee
)
rw this,
end
Table 23: Example of TG-2

---

1emma Trigo_2 (=0:cos(-pi/21f 0) (h1: (2xco (-pt/2111 0) :-cos (0) +cos (229xp1/2)
+ (0) sin (-2////)))0
begin
have -cos(0) (0) (22 sin(0) (sin(-pi) / (2*cos (-pi/2))) -cos (0)
*cos (229xp1/2) (inp)) (2
c2+c0s (-pi/2))
field_simp at "
[to_ 1hs, this,),
have sin(-pi/2) sin(-pi) ( cos(-pi/2)
have sin(-pi) (2x
apply cengr_ arg, ring,
b this,
zw sin_two_mul, field_simp at *,
ring,
conv [to [to_lhs, rw this,
have : (0) -cos (229xpi/2) sin(0) sin(-pi/2) -cos (0) cos (229.
+ (in
{
field_simp at *
b
conv [to_ ths, Iw +- this,), have : cos (-pi//) -cos (229xpi/2),
{
rw cos_ee_neg_cos_dtt aed__ddd_____eeeeeeeeeeeeeeaaaee paruu__tto_p___d__e (-pi/2) (57),
focus/repeat (apply congr_are 11, simp, ring,
h
conv [to_ IM + this,),
have : (0) (-in(-)i/2) cos (0) *cos (-pi/2) (cos + sin(0) vsin (-pi/2),
Heldssing at
conv (to 1hs, this,), have (p:/2) sin sin (-p1/2) cos (0) cos (-p1/2)
have 12) cos (0) (-p1/2)),
apply congr_arg, ring,
1,
this, cob_sub, ring,
b
conv (to_ Ihs, this,),
have : cos (21
Iw cos_pi_div_ttwo
Fw this,
Table 24: Example of TG-3

---

lemma Trr.go____HOEW_eee -2*sin (709+p1/12) +cos (709xpi/12) =- = begin have (709pp)))))) cos (709xp1/12))
-2*sin (709xpi/12) coos (70*xpi/12),
simld_simp at
)
conv {to_lhs, rw + this, , have (709 = 2 sin (700xp11112) cos (709xpp/111))
have sin (709xpi/6) (2 (709+p)11)1)
apply congt_arg, ring,
},
rw this,
rw sin_two_mul,
)
conv (to_lhs, zw this, } have : (163+pp//6 -sin -sin(709pi//)),
IW Len__e_neg_sii__ee add_ int
t twol__too__pt p pdd (163+pi/6) (45),
focus(repeat (apply congr_arg ,/, simp, ring,
}, conv [to_lhs, rw this, have : (23+2p))/66 sin(163ppi/)),
rw sha.epeeiinnggg.adddiii.attt.ttp focus (apply congr_arg , simp, ring,
(23xpi/6) (15),
}, conv [to_lhs, rw this, ) have sin (23xpi/6) -sin -sin(pi/)),
IW tttpg_iinnee_edd_ittn______o___e int _nt_mml__________eee_dde______ int__m____t__ppt (23xpi/6) 6) (2), repeat (apply congr_arg _), simp,
linarith,
},
rw this, rw sin__ii_di___pppppp pi__ivsix
numm_num, end
Table 25: Example of TG-E

---

1emma Trigo_169 (= sin(-pi) " cos(-pi) 2:- begin
have : cos (-2+pl) (694p1/2),
rw cos_eg_sin
(-2+pi) (18),
focus (repeat (apply congr_arg _)), simp, zing,
b
conv
rw +- this, )
have : cos (-2xpi) sin (in(-pi) xx + cos (-pi) x* 2,
{
have cos (-2xpi) - c2+ (-p()))
apply congr_arg, ring,
b,
this, Iv cos_two_mul', ring,
zw this, end
Trigo_80 61 2 sin(31/3) 2:= begin have cos (2-pi/2) (4755pp//)))
lemma
cos eq add div two add int mul two (2xp1/3) (39), reeest (apply congr_arg _), simp, ring,
b conv ths_ this, sin (pi/3) 2,
have : cos (2-p1/3) {
have cos (2xpi/3) cos (2+ (pi/3))
apply congr_are ring,
b
rw this,
Tw 6os cos_two_mul"",
b
2w this,
end
Please simulate the above two proof's and write code to prove the following lemma with theorem proving language Lean.
Please enter code edit box.
lemma (181vppi/) #cos (pi/ =cos (-pi/3) 2 + cos / 2:
Table 26: Examplers for GPT4

---

lemma Trigo_209 sin pi (pi 6) cos(-pi 3) cos (0) / 2 := begin
have h1 sin(181 pi / 3) cos (pi / 3),
IW cos_eg_sin_add_1 pi piddiiitto___dee int www_mmul__tttt_ (pi / 3) (30), focus (repeat (apply congr_arg _)}, simp, ring,
have h2 (pi 6) spn / pi / 6),
Iw sin_ee_cos__nteeee add pi bi__div_to_subbeeeeeee__ (pi pi 6),
},
rw [hi, h2l, have by pi / 3 pi / 2 pi / 6,
apply eq. eq. symn,
Iw simp,
neg,
}
rw hgr
have h4 cos (pi / 2 pi / 3) = cos (-pi / 3) / 2 + cos (0) / 2,
cos_half_angle__en
simp, ring,
),
rw h4,
end
Table 27: Output of GPT-4.

---

1emma Trigo_210 : sin(pi/)) *cos tain +cos (pi/6)
=sqrt /3)
begin have
sin (2xpi/3) = sin(pi/6) cos (pi/2) + sin(pi/2) cos (pi/6),
have
sin (2xpi/3) sin((pi/6) (pi/2)),
apply congr_arg, ring,
)
rw this,
rw sin_add,
ring,
),
conv {to_lhs, rw this, h have : (2xp111) sqrt 3 2,
Iw sin_tto__i_
}
rw this,
end
Please use the theorem proving language lean to imitate the above example to prove the following lemma:
lemma Trigo_254 :
#cos (s/1/// (cos (11+pi/122)
= sqrt
begin
have
sin (3 - -sin (11 (11xp11111) xoos ( (-pi/6) (sin (-pi/6) xoos (11*pi/ /
have sin = sin ( (11xpi/122 (-pi/6)),
apply congr_arg, ring,
},
rw this,
Iw sin_add, ring,
),
conv [to_lhs, zw this,
have : (3xp1/1) sqrt ( 2
2,
Iw sin_three_pi_ccv_fou
b,
rw this, end
Please use the theorem proving language lean imitate the above example to prove the following lemma:
lemma 2rigo_436 : -sin (37)+p1/2)=sin (-2+pi)
(pi/2) sin (pi/2)
coS (-2+pi) =
Table 28: Examplers 2 for GPT-4

---

begin have : -sin s-n(-2pi) cos (pi/2) (pi/2)
cos (-2pi),
have : -sin (379pi/2) sin (i-p())))) (381pi/2)),
apply congr_arg,
rw [mul_comm (-2) pi, mul_comm (381/2) pil, ring,
)
rw this, rw sin_add, ring,
b
conv [to_lhs, rw t- this, }
have -sin (379pi/22) = sin (pi/2))))
peg_siin_prriodicit,,
Iw mul_comm,
have (379 (pi / 2)) (2 pi) pi 2,
we have 379pi/2 = 189xpi + pi/2 sub_mul, add_halves),
rw d___sub_iff_ad___e
have : 379 = 2 * 189 + 1, by linarith, zw [this, mul_add, mul_one, add ads_as)oc),
}
rw this,
},
rw this,
end
Table 29: Output 2 of GPT44.

---

lemma Trigo_169 : (in -- sin(-pi) ** cos (-pi) x 2:
begin
have : cos (-2+pi) = sin(69xpi/2),
cos_e___in__dd____dttz htttttoo_dd____eeeee int mul_ _ul__wooppi (-2xpi) (18),
focus (apply congr_arg _}},
simp,
ring,
} conv [to_lhs, zw + this, } have : cos (-2xpi) = - sin (-pi) xx 2 + cos ** 2,
have cos (-2xpi) = c2+ (-pi)),
{
apply congr_arg, ring,
}
rw this,
rw cos_two_mul',
ring,
)
rw this, end
1emma Trigo_80 sin(475+pi/6) spn/3)))) 2: begin
have : cos (2*pi/3) = sin (475+pi/6),
IW si________ddd____i bod__pidvv_to_aadee woo. int mul t_to__o_pip (2xpi/3) (39), frcpst (apply congr_arg | simp, ring,
}, conv [to_lhs, rw this,),
have : cos (2xpi/3) = 1 2 sin (pi/3) ** 2,
have : cos (2xpi/3) = (2x (pi/3)
apply congr_arg, ring,
},
rw this,
IW cos_two_mul",
b
rw this, end
Please simulate the above two proofs and write code to prove the following lemma with theorem proving language Lean. Please enter the code edit box.
Table 30: Examplers for GPT-3.5

---

lemma Trigo_260 : con cos (pin cos (pi/6)
begin
have : cos cos = sinn(pi//) cos
cos (pi/6),
repeat (rw [mul_comm (cos _11,,
have eql 181pi/3 = 60 + pi/3, ring, rw sin co. zerommul, zero, neg_zero,
www.ppp.dl__ttoocc_pp_ddddi/ rw cos_zero), rw [cos_add, cos cos_div_sqrr_thhreee sin sin_divv_ss__eeeeeeeeeeeeppsisss div_ssgrt_hhree,
mul mul_one, cos dil__ii__aat six],
litbb_pi_dv_____ieeeel div pi,
mul_div_canceelleft (show (2 # 0), by norm_num)), rw sin cos cot.ppp..il_._ge______________. neg_zero, cos_pi_div_two, mul_one, rw [ssii_.eeg_co__muupppp......y..u sin cos_zero), Iw http:accccc__ddiv_ssttttttteeeee mul_div_cancel_leff (show (2 # 0), by norm_num)), ] ring,
otgp:p/ww.....auuuooo..oooooooo. div__ddiiiii two pi,
cos
}, rw this, rw [cos_ec_sin_edd____dir__ (-pi/3), cos_eq_sin_add pi_ sei_div_twe too 0, sin_pi_div_six cos vos_pi_div_sin ring, end
Table 31: Output I of GPT-3.5.

---

1emma Trigo_210 : sin(pi/)) ccss(p///) sin(pi/2) +cos (pi/6)
=sqrt /3)
begin have
sin (2xpi/3) = sin(pi/6) cos (pi/2) + sin(pi/2) cos (pi /
have
sin (2xpi/3) sin((pi/6) (pi/2)),
apply congr_arg, ring,
)
rw this,
rw sin_add,
ring,
),
conv {to_lhs, rw this, h have : (2xp111) sqrt 3 2,
Iw sin_tto__i_
}
rw this,
end
Please use the theorem proving language lean to imitate the above example to prove the following lemma:
lemma
Trigo_254 : (1n
#cos (-p// (cos (11+pi/122)
=sqrt (2)
begin
have : sin (3xpi/4) - -in (11 (11xp1/11) xoos ( (-pi/6) (sin (-pi/6) xoos (11*pi/ /
have sin = sin ( (11xpi/122 (-pi/6)),
apply congr_arg, ring,
},
rw this,
Iw sin_add, ring,
),
conv [to_lhs, zw this,
have : (3xp1/1) sqrt ( 2
2,
Iw sin_three_pi_ccv_fou
b,
rw this, end
Please use the theorem proving language lean imitate the above example to prove the following lemma:
lemma 2rigo_436 : -sin (379+p)/2)=sin (-2+pi) (pi/2) sin (pi/2)
coS (-2+pi) =
Table 32: Examplers 2 for GPT-3.5

---

begin oss.aagg.....egn.........p..o..r half, co._p__aaif,,errmmmmdddd___._e__
rw [sin_pi, cos_ neg neg_ add end
Table 33: Output 2 of GPT-3.5.
import data. .bssi import analysis. special - www.gooetttiri.bbaa.....
open real
lemma Trigo_5 -sin (538 real.pi
cos cos (433 real.pi 6)
begin
Use the fact that sin + real pi/2) cos (x) and cos (x + real.pi/2) = (xn
have h : cos (433 * real.pi / 6) -sin (433 * real.pi / 6 + real pi / 2),
{ rw cos_add_
,
Simplify both sides of the equation
have h : 433 real.pi / 6 538 real 3, { rw @div_ee_div_ifte cul_comm 433, mul_comm 538], norm_num },
substitute h into h have h : cos (538 * real.pi / 3) -sin (538 * real.pi / 3 + real pp / 2),
{ rw [+h h b
Now, we use the periodicity of the sine function: sin (x) for any integer have h : sin (538 * real.pi 3) sin(538 real.pi.
sin pi
* real.pi * 179),
{ Iw interiioiiciittmmulle
pi 179 h
Simplify the right-hand side of h have h : 538 real.pi / 3 real pi 179 538 real.pi real.pi / 2,
rw [div_eq_die div iff, mul_comm 538, mul_comm comm 3], norm }
Combine h h and h to get the final result rw h h h 1, end
Table Zero-shot test case of GPT-4.

---

import
import ottpeaaaioitttioooo..oooooeoeeno trigonometric.....o..o.......i.t basic
open real open_locale real
1emma Trigo_0 : (107 * T)) : begin
--
Use the periodicity of the sine function and
the fact that sin =0 for any integer have h sin (107 * T = sin(x 107),
{ rw mul__com
Apply sin int int_miit/ mum_ml_p pi rw [h, sin_int_mul_pi]
end
Table 35: Zero-shot test case of GPT-4.
import reta.real.base.
import
lemma Trigo_5 : -sin (538 * real.pi / 3) cos (433 real / 6) begin
IW [K-subeeg_zero, sinn_ree, sub_neg_eg_add com_, sin_add],
Iw [div_mul_comm sin sin_int_mmi inniit__mlli,, cos int mul pi, mul_zero, sub_zero, add_zero, mul__nee], rw [div_mul_comm, cos_int_mul_pi, sin iin_int_mul_ph mul_zero, sub_zero, add_zero, mul_one], simp only [int cast_add, int.cast cast__ub,, cas.cast_bit0 int cast_ cast_one), norm_num, end
Table 36: Zero-shot test case of GPT-3.5.
import lata.real.basia import trigonometry.com w angle
lemma Trigo_0 : sin (107 m) := begin
rw [mul__oom,, mssoca -sin_int_add_ptt sin_pi],
norm_num, end
Table 37: Zero-shot test case 2 of GPT-3.5.

---

common_cclc__teer
"focus (apply congr arg , "try (simp)", "ring"
congrarg_linarfte "[", "apply congr_arg", "ring", "),",
class sin_two__tt two www_ww_odeeooooooooo _ii__to_pi_div_thres def Siiit (slfi se self.rule "sin (srt (3)/2"
self.no_mapping True se selt.nas_nonzere False
def gat_tactics (self, mapping, left, right): return ("sw sin_tro_pi_di__hrreee
tan_add_inn class tan add int m___m_1ppp _o__add_aat_mm______
dof inii (scif] se self.rule solf.has_noneee
(x) (x)-tanppix x)"
False
def get_tactics (sel,,,, (self, mapping, left, right): k, _ [KK, mapping[X]
steps -
f'rx tan eq tan adá int mul på ((x)) (LK)),, cowmon_ccalliccccooooooooooooose common_calc_steps
] return steps
class sin_nog_add_in__mmttveee.e
def _nnit_
self.ruls "sin (X)= + (2* 1))"
self.has_nonzers = False
def sec_tacticssset mapping, left, right): 3, map mapping[x]
steps
f'rw sin_eg_sin_nee__ee htt___________________eeeeeooo ttt______twtt___d_________ ((x)) ((.))), common_callestepp
return steps
class
def init (self):
self.rule (2xx (X)
self.has_nonzen False
def get_tactics (self, mapping, left, right):
_ mappinglX]
have_goal f"have : sin ((2x_x)) (in(2 steps
have_goal,
1 congrarg linarith + "rw this", "rw sin two het_tto__mly mul", "try (ring)"
return steps
Table 38: Examples of mapping rule to tactics. The Python classes corresponding to each rule are listed below, with the "get__tatics" tactics' method used to return their corresponding tactics. 'self.rule' specifies their corresponding rule, "sllf.no_mapping' specifies whether replace the parameters X, Y, K in the rule, and _asf.eass_onzeroo whether to include the condition that the denominator is not zero before proof.
nonzero' specifies


Reviews:
[{"review_id": "OSFNnKgb4Q", "reviewer": "Reviewer_Gc1T", "summary": "", "questions": "- Please elaborate more on the recruitment of the annotators and Ph.D. students completing the proofs. How were they selected, how much human effort was putting into this dataset?\n- I browsed through the tiku website. Most of the questions were ‘fill in the blanks’ type of questions, how exactly was the data gathered, please elaborate\n- What are the “different” websites on page 3, line 205?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "#### To Reviewer Gc1T: \nThank you for your thoughtful comments and detailed feedback.\n**Question 1: The dataset is limited in size, making it only usable for fine-tuning.**\nResponse: \n\nThe dataset we have created is used for fine-tuning and testing the model's ability to perform mathematical reasoning involving complex combinations of numbers. We achieve this by manually collecting exam questions from the real world, annotating their simplification processes, and formalizing these processes. Additionally, we control the complexity of proof problem by manipulating their distributions, including numerical value ranges and proof difficulty. Lastly, we assess the model's generalization capabilities on both synthesized and real world problem. Due to resource constraints, we are unable to annotation large amouts of data for large scale pre-training.\n\n**Question 2: The comparison to GPT-4 is unfair, this needs to be more clearer in the paper (because despite the introduction/abstract, I doubt that GPT-4 has seen that much Lean).**\n\nResponse:\n\nFirstly, we believe that Large Language Models (LLMs) such as GPT-4 have already shown the capability of processing formal language, particularly in the context of translating the informal proofs to formal proofs [1,2]. Furthermore, as indicated in reference [3], LLMs have substantial potential  in proving formal theorems with proof assistants like Lean. [3] demonstrated that GPT-4 can generate proofs accepted by Lean in a zero-shot manner, establishing GPT-4 as a strong baseline. These  results indicates the possibility of Lean example exists in the GPT-4 training corpus as numerous proofs were publicly accessible on GitHub prior to GPT-4's data cutoff date (September 2021) [4].\n\nThe purpose of introducing GPT-4 is to explore the limits of language models in tasks involving complex numerical comprehension. For instance, as shown in Figure 2, we initially probed GPT-4's performance in completing entire proofs with human feedback errors. Subsequently, in Table 5, we delved into GPT-4's ability to complete single-step proofs. Furthermore, in Appendix L, we demonstrated GPT-4's capability to complete an entire proof in a single attempt when provided with a 2-shot complete proof. The above experiments have shown that gpt-4 is capable of generating partially correct proofs on TRIGO. However, it still exhibits common phenomena of language models such as hallucinations and inability to accurately provide equations. This suggests that our dataset poses a significant challenge for GPT-4.\n\nWe will include the above analysis and clarification in the revised version to justify the reason of evaluating GPT-4 on our proposed TRIGO.\n\n\n\n**Question 3: Please elaborate more on the recruitment of the annotators and Ph.D. students completing the proofs. How were they selected, how much human effort was putting into this dataset?**\n\nResponse:\n\nOur annotation team consists of four Master's students and three PhD students. The Master's students are responsible for completing the annotation of informal proof steps, while the Ph.D students focuse on formalizing the informal proofs into Lean. The four Master's students holds a Master's degree in Computer Science. They have received rigorous mathematical training and possess in-depth knowledge in the process of reducing trigonometric expressions. The three Ph.D students are in the field of computer science specializing in formal theorem proving. Four Master's students firstly simplify the trigonometric functions, then Ph.D students manually translate these informal proofs to Lean and submit them to the Lean theorem prover for correctness checking. The combined process of data annotation and mathematical formalization took one month to complete.\n\n**Question 4: I browsed through the tiku website. Most of the questions were ‘fill in the blanks’ type of questions, how exactly was the data gathered, please elaborate.**\n\nResponse:\n\nWe instructed the annotators to collect problems related to trigonometric expression reduction from the trigonometric section of the \"tiku\" website. For the fill-in-the-blank questions, we asked the annotators to gather the corresponding expressions and answers. Once collected, annotators manually filtered out questions whose answers did not match the expressions. If the collected questions lacked a reduction process (such as in the case of fill-in-the-blank questions), we required annotators to use an interactive annotation system to annotate the specific reduction steps.\n\n**Question 5: What are the “different” websites on page 3, line 205?**\n\nResponse:\n\nWe utilized search engines to gather questions from various websites, including  https://www.51jiaoxi.com/, https://wenku.baidu.com/, and also from high-school math exam papers provided at https://www.gaokao.com/zyk/gzsj/. Our intention was to avoid collecting questions solely from a single source, and  to obtain a diverse range of questions.\n\n>[1] Wu, Yuhuai, et al. \"Autoformalization with large language models.\" Advances in Neural Information Processing Systems 35 (2022): 32353-32368.\n\n>[2] Jiang, Albert Q., et al. \"Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.\" arXiv preprint arXiv:2210.12283 (2022).\n\n>[3] Yang, Kaiyu, et al. \"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models.\" arXiv preprint arXiv:2306.15626 (2023).\n\n>[4] GPT-4 Technical Report.", "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": "- Studying mathematical reasoning capabilities of LLMs is an important research direction\n- Useful datasets are rare, the authors contribute to the data scarcity problem\n- I see the most value of this dataset in the manual annotation effort done by Ph.D. students (page 4, line 288+)\n- Experimental results show that the dataset can be used to effectively train even small LLMs; promising results", "reasons_to_reject": "- Some of the results are not surprising (with more human-level input, the model will improve in distribution)\n- The dataset is limited in size, making it only usable for fine-tuning\n- The comparison to GPT-4 is unfair, this needs to be more clearer in the paper (because despite the introduction/abstract, I doubt that GPT-4 has seen that much Lean)\n", "questions_to_authors": "- Please elaborate more on the recruitment of the annotators and Ph.D. students completing the proofs. How were they selected, how much human effort was putting into this dataset?\n- I browsed through the tiku website. Most of the questions were ‘fill in the blanks’ type of questions, how exactly was the data gathered, please elaborate\n- What are the “different” websites on page 3, line 205?", "paper_topic_and_main_contributions": "In this submission, the authors present TRIGO, a dataset of trigonometric expressions for training and studying the performance of LLMs on reducing these expressions. The authors describe their data gathering, data annotation (proof completion), and data generation process before providing experiments showing that training GPT-2 models on this dataset learn to reduce trigonometric expressions effectively (even compared to GPT-4, although this comparison is a bit unfair).\n", "excitement": 4, "reproducibility": 2, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"Typos_Grammar_Style_and_Presentation_Improvements": "There are a few grammar issues, especially later in the paper, and in lines 68-87 on page 1. I would recommend running a checker."}, "extra_text": {}}, {"review_id": "HmdA5gKshB", "reviewer": "Reviewer_W12Q", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 2, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "#### To Reviewer W12Q\n\nThank you for your thoughtful comments and detailed feedback.\n\n**Question 1: Is the automatic proof generation the main methodological contribution?**\n\nResponse:\n\nOur main contribution is the TRIGO benchmark, which is an evaluation framework for language models on formal mathematical reasoning with complex numerical inference. The benchmark construction involves automatic proof generation techniques to create training and testing sets spanning various difficulty levels. Throuhg the generation program, we can control the theorems sampling distribution, generate question with desried difficulty, and verify the correctness of the proofs automatically. Additionally, we also utilize automatic proof generation directly on TRIGO-real to expand the scale of the training dataset.\n\n**Question 2: Is it possible to train on Trigo and have performance improve on other proof benchmarks?**\n\nResponse:\n\nThank you for your valuable suggestion. Due to time and computational resource limits, we currently unable to include this experimental results here. However,  we are glad to evaluate whether the TRIGO sample can improve models’ performance on other benchmarks and include the results in the revised version if possible.\n\n**Question 3: It would be great to specify the websites, the number from each website, and why additional sourcing was needed, since it seems that the total dataset size did not increase by much.**\n\nResponse:\n\nThe questions collected from other websites refer to the websets found through search engines, including https://www.51jiaoxi.com/, https://wenku.baidu.com/, and https://www.gaokao.com/zyk/gzsj/. These sources contain high school math exam questions with standard answers. Throughout the collection process, we aimed to gather data randomly whenever possible, ensuring diversity in the distribution of the test set. The additional collection of TRIGO-web was conducted with the goal of obtaining a more extensive test set and a broader range of sources to reflect the model's performance on real human exam questions.\n\n**Question 4: It would be great to show some examples, such as screenshots, of the annotation software and flow. It’s also not clear if the annotators during this step are the authors themselves, or if there were other annotators.**\n\nResponse:\n\nIn Figure 7, we present screenshots of the annotation software and its workflow. The formalization process of trigonometric function proofs includes the authors, but the process of annotating the steps for trigonometric expressions reduction does not involve the authors. \nSpecifically, our annotation team consists of four Master's students and three PhD students. The Master's students are responsible for completing the annotation of informal proof steps, while the Ph.D students focuse on formalizing the informal proofs into Lean. Four Master's students firstly simplify the trigonometric functions, then Ph.D students manually translate these informal proofs to Lean and submit them to the Lean theorem prover for correctness checking. \n\n**Question 5: It would be great to attach an appendix to Section 4.3 to clarify on which additional steps that PhD students had to fix. And again, it would be great to specify how they differ from the initial annotator pool.**\n\nResponse:\n\nThank you for your valuable suggestion. In the revised version, we will attach an appendix to Section 4.3 to provide clarification on the additional steps that Ph.D. students had to address. The initial annotator pool was tasked solely with annotating specific trigonometric expressions reduction processes. After annotating the reduction process, Ph.D. students translate the informal proof to formal proof with Lean.", "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": "The paper contributes new data resources for mathematical proof reduction. Trigonometry seems to be a relatively underexplored area in proof datasets. The paper presents relatively thorough experiments to understand the gaps between the curated and generated datasets. The paper also assess the impact of different proof search algorithms, expert iteration, and an expanded set of angles.\n", "reasons_to_reject": "Although it’s a well-curated dataset and it’s always important to contribute additional benchmarks, the specifics of the impact are not clear to me from reading the paper alone. Is the automatic proof generation the main methodological contribution? Is it possible to train on Trigo and have performance improve on other proof benchmarks?\n\nSome of the steps of the dataset curation process could be described with more precision.\n* Line 203: “To expand our dataset, we further collect additional trigonometry reduction problems from different websites.” It seems like only a small percentage of problems were sourced from outside Tiku. It would be great to specify the websites, the number from each website, and why additional sourcing was needed, since it seems that the total dataset size did not increase by much.\n* Section 4.2 It would be great to show some examples, such as screenshots, of the annotation software and flow. It’s also not clear if the annotators during this step are the authors themselves, or if there were other annotators. \n* It would be great to attach an appendix to Section 4.3 to clarify on which additional steps that PhD students had to fix. And again, it would be great to specify how they differ from the initial annotator pool.\n\n", "questions_to_authors": "", "paper_topic_and_main_contributions": "This paper contributes new data resources for the evaluation of formal mathematical proof reduction capabilities. The paper primarily describes the data curation process. It also presents some evaluations of GPT-2 and GPT-4.\n\nTrigonometry problems are first sourced from Tiku, an open online repository of math problems across elementary, middle, and high school levels. First, a pool of annotators write out the step-by-step reduction process. Then each step is translated into the Lean formal language. Finally, additional problems are generated in Lean by using pre-existing rules, and substituting values (e.g. pi/2 for pi/3).\n", "excitement": 4, "reproducibility": 4, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"Typos_Grammar_Style_and_Presentation_Improvements": "Line 62: trigonometric\nLine 139: Should citet instead of citep\n"}, "extra_text": {}}, {"review_id": "MXGGrOgjKr", "reviewer": "Reviewer_ET7v", "summary": "", "questions": "How do you ensure the quality of the annotated data and the agreement between annotators?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 4, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "#### To Reviewer ET7v\n\nThank you for your thoughtful comments and detailed feedback.\n\n**Question 1: I believe the paper would benefit from a deeper discussion on how the quality of the generated dataset is verified. For example, human annotation is involved, but I could not find any discussion or report of inter-annotator agreement and quality check. How do you ensure the quality of the annotated data and the agreement between annotators?**\n\nResponse:\n\nWe use Lean-Gym and Lean verifier to ensure the genearted and annoated proof is correct.  Specifically, for the generated proof, we only retain those proof that can reach a \"no goals\" state (indicating a correct proof) when interact with Lean-Gym. For annotated data, we submit them to Lean verifier and perserve the data that can pass the verification process.\n\nWe consider a correct annotation also has relatively high qualtiy. Unlike some other tasks whose annotation is subjective and largely varies among annotators, the formal envrioment provides a rigorous and objective evaluation. If a annotation can pass the verifier, all annoator will agree the annoation is correct, leaving no room for ambiguity. Thus, we do not calculate the inter-annotator agreement (IAA) or observer consistency similar to other tasks, but use verifier to ensure the correctness of the annoated proof. We will include the above discusion in the revised version.\n\n\n**Question 2: The evaluation is performed using a single family of generative models (i.e. GPT). As GPT4 is not freely available to the community and much of the details are unknown, I believe the experiments would benefit from an additional comparison between open models (for instance comparing GPT2 with T5).**\n\nResponse:\n\nDue to resource and time constraints, we only conducted experiments using T5-base on TG-real and TG-1, TG-2, TG-3. The detailed experimental settings are as follows: we set the maximum number of training epochs to 5, the initial learning rate to 5e-5, and used a linear learning rate scheduler. The batch size was set to 512, and we trained the model using 8 V100 GPUs. However, We found that T5-base only successfully completed a full proof on the simplest subdataset TG-1. Therefore, we conducted experiments and analysis on its single-step proof, and the experimental results are as follows:\n\n|        | TG-1  |  TG-2  |  TG-3  | TG-real  |\n|  ----  | ----  | ----  | ----  | ----  |\n| T5-base all-proof  | 74.1 | 69.1 | 65.0 | 48.7 |\n| GPT2-base all-proof  | 95.8 | 92.1 | 89.3 | 66.1 |\n| T5-base have  | 90.2 | 81.1 | 76.6 | 3.2 |\n| GPT2-base have  | 92.4 | 82.9 | 78.9 | 11.4 |\n| T5-base w/o have  | 69.5 | 65.3 | 61.3 | 60.3 |\n| GPT2-base w/o have  | 96.5 | 94.8 | 92.4 | 79.2 |\n\nThe terms \"all-proof,\" \"have,\" and \"w/o have\" in the above table refer to the following: \"all-proof\" represents all single-step proofs filtered from TG-1, TG-2, TG-3, and TG-real datasets. \"have\" indicates single-step proofs that include the \"have\" tactic. \"w/o have\" refers to single-step proofs that do not include the \"have\" tactic. We conducted experiments to compare the performance of the gpt2-base and T5-base models on single-step proofs. We observed that they exhibited similar performance on the most difficult proofs, which involved stating the proof subgoals and included the \"have\" tactic. The primary performance difference between the two models was seen in the tactics that did not include the \"have\" tactic. On the program synthesis dataset, T5-base demonstrated an average accuracy that was 29.2% lower than gpt2-base, while on TG-real, its accuracy was lower by 18.9% compared to gpt2-base. The lower performance of T5-base on tactics that do not include the \"have\" tactics has led to difficulties in completing a full proof. We will include the above results and analysis in the revised version.", "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": "- The paper is very well-written and well motivated\n- TRIGO represents an extensive resource that can support future research on the evaluation and improvement of the mathematical and symbolic reasoning capabilities of Language Models and Machine Learning approaches in general. \n- The paper proposes an original methodology for data generation that combines human experts with a formal environment. The proposed methodology can serve as an inspiration for future work in the field.\n- Extensive empirical evaluation on state-of-the-art models.", "reasons_to_reject": "- I believe the paper would benefit from a deeper discussion on how the quality of the generated dataset is verified. For example, human annotation is involved, but I could not find any discussion or report of inter-annotator agreement and quality check. \n- The evaluation is performed using a single family of generative models (i.e. GPT). As GPT4 is not freely available to the community and much of the details are unknown, I believe the experiments would benefit from an additional comparison between open models (for instance comparing GPT2 with T5). *Update*: This limitation is partially addressed in the authors's rebuttal with new results.", "questions_to_authors": "How do you ensure the quality of the annotated data and the agreement between annotators?", "paper_topic_and_main_contributions": "The paper explores in detail the problem of Trigonometric Expression Reduction (TRIGO) with Language Models, a task that can be used to develop and evaluate symbolic and numerical reasoning capabilities that are necessary for Automated Theorem Proving (ATP) and mathematical reasoning in general. \n\nThe paper proposes a new resource, named TRIGO, along with a data generation methodology that combines expert annotation with a formal environment (Lean). Specifically, TRIGO is composed of three subsets, TRIGO-web, TRIGO-real, and TRIGO-gen, that combine synthetic and real-world data to train and test models on problems of different complexity and investigate out-of-distribution generalisation. \n\nThe authors provide an in-depth evaluation and analysis of the performance of generative models, combining GPT2 with a proof search algorithm, and exploring the limitations of GPT4.", "excitement": 4, "reproducibility": 3, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper provides a benchmark measuring how well ML language models can reduce formal mathematical proofs.

Pros:
- Understanding mathematical reasoning capabilities of ML language models is a relevant task, even before the advent of ChatGPT, but even more important now that users commonly expect language models to assist with maths-related topics.
- The datasets, algorithms, and code are openly available and will be useful to the community.
- Well-written and well motivated.
- Proposes an original data-generation methodology combining human experts with a formal environment; can inspire future work.
- Extensive empirical evaluation on state-of-the-art models.

Cons:
- Somewhat small data set, perhaps restricting the use case to fine-tuning only. 
- Manual annotation effort is not super clearly described, but additional details were provided in the review threads and these could be included into the paper.
- Some concerns around clarity and fairness of experiments involving GPT-4, which were addressed in the review threads and clarifications could be incorporated into the paper.
Decision: Accept-Main