2506.10558

# StepProof: Step-by-step verification of natural language mathematical proofs **Authors**: - Xiaolin Hu (School of Computing and Mathematical Sciences) - Leicester, UK - &Qinghua Zhou (Department of Mathematics) - London, UK - &Bogdan Grechuk (School of Computing and Mathematical Sciences) - Leicester, UK - &Ivan Y. Tyukin (Department of Mathematics) - London, UK Abstract Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization—the process of translating natural language proofs into formal proofs that can be verified. Despite these advancements, existing autoformalization approaches are limited to verifying complete proofs and lack the capability for finer, sentence-level verification. To address this gap, we propose StepProof, a novel autoformalization method designed for granular, step-by-step verification. StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification. Experimental results demonstrate that StepProof significantly improves proof success rates and efficiency compared to traditional methods. Additionally, we found that minor manual adjustments to the natural language proofs, tailoring them for step-level verification, further enhanced StepProof’s performance in autoformalization. Our project is available on https://github.com/r1nIGa/STEP-PROOF K eywords Autoformalization $·$ Theorem Prover $·$ Natural Language Processing 1 Introduction Mathematics is the basic tool for the development of science, and the reliability of its conclusions affects the stable growth of various disciplines. With the development of the mathematical edifice, mathematical proofs have become more complex and lengthy. The verification of mathematical proof often requires years of careful verification to ensure the accuracy of the work. However, reading a mathematical work requires a large amount of knowledge, and in the face of the many branches of mathematics today, traditional manual verification has become increasingly disastrous. Thus, an idea arose to validate mathematical work written in natural language automatically. At present, there are two kinds of automatic verification of mathematical proof. One is to write the mathematical certificate into a machine code that can be verified by a specific expert system, which is called the interactive theorem prover (HARRISON2014135, ). After more than 40 years of development, the interactive theorem prover has begun to take shape and has been used in the verification of many mathematical works (maric2015survey, ). However, because such machine-verifiable proofs need to be written in a specific programming language, whose learning cost is relatively high, interactive theorem provers are only used by a small number of mathematicians at present (nawaz2019survey, ). On the other hand, after the advent of the large language model (zhao2023survey, ), through prompt engineering (liu2023pre, ) and few shot learning (wang2020generalizing, ), large language model can be applied to many natural language processing tasks, and achieved considerable performance (achiam2023gpt, ). However, due to the hallucination problem of large language model (ji2023survey, ), its performance in mathematics and strong logic-related work is not good enough (huang2023large, ), so the lack of reliability of large language model to verify mathematical work is easy to cause a lot of errors. In this context, a method that combines large language models and theorem provers gradually comes into people’s view, which is called autoformalization verification (li2024survey, ). At present, the existing automatic formal verification work generally adopts a FULL-PROOF strategy. Although such a strategy has achieved some impressive performance in some studies, there are still many problems in the stability of its proof and the fine-grained verification. Aiming at the problems existing in FULL-PROOF, we innovatively propose a new automatic formal proof strategy, STEP-PROOF. And the performance of StepProof is better than traditional methods in several aspects. In summary, our contributions mainly include the following points: 1. We pioneered a novel natural language mathematical verification method StepProof, which realizes informal mathematical proof verification at the sentence level. 2. We were the first to realize the test of automatic formalization capabilities on small open-source LLMs. 3. Compared with existing methods, the StepProof method has been significantly improved in all aspects of performance. In this paper, we will first make a brief summary of the existing relevant works and the technical background in Chapter 2. In Chapter 3, we will give a detailed introduction to the two types of strategies, FULL-PROOF and STEP-PROOF, and point out many problems faced by traditional methods. In Chapter 4, we set up a series of experiments to verify the performance of STEP-PROOF in verification tasks and its superiority over FULL-PROOF. At the same time, we also carried out a detailed analysis of some phenomena observed in the experiment to further explain the reason for the advantages. In the end, we analyze and look forward to the current limitations and future development direction. 2 Related Work Theorem Prover: Theorem provers can be roughly divided into two types, interactive theorem provers (ITPs) in which the user can enter and verify the existing proof (asperti2009survey, ), and automated theorem provers (ATPs) that try to prove the statements fully automatically (harrison2013survey, ). The two types of theorem provers are not mutually exclusive (nawaz2019survey, ). Most ITPs such as Isabelle (paulson1994isabelle, ), Coq (huet1997coq, ) and Lean (de2015lean, ) are supported by ATPs that try to automatically prove ”obviously” intermediate steps in the proof entered by the user. The entered proofs are rigorously verified back to the axioms of mathematics. Different ITPs use different axiomatic foundations, e.g. set theory, first-order logic, higher-order logic, etc. Each ITP use its own language and syntax, which makes the learning cost of theorem prover high, and precludes ITPs from being widely used (yushkovskiy2018comparison, ). Large Language Model: In recent years, large language models (LLMs) have achieved outstanding performance in many downstream tasks of natural language processing. LLMs such as Llama (dubey2024llama, ), GPT series (ye2023comprehensive, ) and GLM 4 (glm2024chatglm, ) are trained on large databases to understand user input in natural language and produce the related output. While large language models perform well in general tasks such as translation, their performance in dealing with logic problems has been limited. A lot of work has also shown that large language models are prone to a variety of problems when dealing with logic problems (yan2024large, ; wan2024b, ). Although in the subsequent iteration of the model, the developers provided a large amount of high-quality logic-related data to improve the logic capability of the model, the effect that could be achieved was still very limited (lappin2024assessing, ). Therefore, it has become a trend to add an expert system to the model to improve its accuracy, such as RAG (fan2024survey, ), which is currently commonly used in question-answering systems. On the other hand, step-by-step reasoning has been proven can improve the reasoning ability of existing LLMs (wei2022chain, ; khot2022decomposed, ), which gives us a hint to apply in autoformalization. Autoformalization: The definition of automatic formalization is very broad, but can be roughly seen as understanding and extracting translation from natural language to obtain the required structured data or formal language, such as entity relation extraction (nguyen2015relation, ). Early automatic formalization work involved extracting logical propositions from natural language in addition to entity relation extraction (singh2020exploring, ; lu2022parsing, ). However, the main problem in this kind of work is that the extracted logical propositions lack corresponding symbols for derivation and application, so the output of the automatic formalization output cannot be directly applied. With the launch of pre-trained language models such as transformer and BERT, language models have a stronger understanding ability. Wang et al. (wang2020exploration, ) conducted an early automatic formalization attempt for the theorem prover Mizar. However, due to the limited size and training expectations of the models at that time, the effects they could achieve were very limited. With the rapid expansion of the scale of models and predictions, many new and better performance automatic formalization work has emerged, such as the Majority Voting method by Lewkowycz et al. (lewkowycz2022solvingquantitativereasoningproblems, ), the DSP method by Jiang et al. (jiang2022draft, )., and the method proposed by Zhou et al. (zhou2024don, ), in DTV (Don’t Trust: Verify). They further improved the automatic formalization of the system by combining large models with some syntax-modifying filters. However, on the one hand, all these works are tested in the closed-source large model Minerva, which lacks the testing work of open source model and small model. Meanwhile, all these works adopt the strategy of FULL-PROOF, which has poor controllability for the formal output of the model, and it is difficult to locate the error point of non-formal proof. Qinghua et al. proposed a problem location method based on the FULL-PROOF strategy in SlideRule. However, this method relies heavily on the format and quality of the generated formal content, so it cannot achieve 100% problem locations detected. To solve these problems, we propose StepProof, an automatic formalization strategy that can realize sentence-level verification, to realize the verification of natural language mathematical proofs. Moreover, LEGO-Prover (wang2023lego, ) proposed a new methodology to decompose the whole proof into several sub-proofs. Although the idea of step-proof is taking shape, it still requires some extra generation of the sub-proof formal statement generation, which increases the error probability of formalization. 3 StepProof In this chapter, we will provide a detailed introduction to the workflow design of StepProof. We will also compare the STEP-PROOF strategy used by StepProof with the FULL-PROOF strategy adopted by existing autoformalization systems, highlighting the problems with traditional strategies and the advantages of STEP-PROOF over FULL-PROOF. 3.1 FULL-PROOF Current research on natural language proofs formal verification predominantly employs the FULL-PROOF strategy, as seen in methods like DSP and DTV. The workflow of FULL-PROOF method can be roughly illustrated as the left of Figure 1. Users submit a provable problem along with its proof process. The problem is first formalized, then the informal problem, the formalized problem, and the entire informal proof are packaged as inputs to a large language model for formalization. After obtaining the formal proof, it is combined with the formalized problem and input into a theorem prover for rule-based formal verification. The verification results are then returned to the user. Despite the clarity and simplicity of the FULL-PROOF workflow, it has significant drawbacks. <details> <summary>extracted/6582548/strategy.png Details</summary>  ### Visual Description ## Diagram: Comparison of Full-Proof and Step-Proof Strategies for Math Proof Verification ### Overview The diagram illustrates two strategies for verifying mathematical proofs: **Full-Proof Strategy** (left) and **Step-Proof Strategy** (right). Both involve natural language math proofs, auto-formalization, and verification, but differ in workflow and error handling. --- ### Components/Axes #### Full-Proof Strategy (Left) 1. **Input**: "Natural Language Math Proofs" (e.g., "Step1, Step2, Step3, ..., QED"). 2. **Process**: - **Auto-Formalization**: Converts natural language proofs into formal representations. - **Checker**: Validates the formalized proof. 3. **Output**: - **Succeed** (green): Successful verification. - **Failed** (red): Verification failure. #### Step-Proof Strategy (Right) 1. **Input**: "Natural Language Math Proofs" (e.g., "[Step1, Step2, Step3, ..., QED]"). 2. **Process**: - **Auto-Formalization**: Converts natural language proofs into formal representations. - **Checker**: - **Verified**: Adds steps to the **Formal Proof Stack** (green for completed steps, yellow for the current step). - **Failed**: Triggers **Regenerate** (user intervention) or **Hold** (pause). 3. **Output**: - **Formal Proof Stack**: Hierarchical structure of verified steps (e.g., "Formal Step 1," "Formal Step 2," etc.). - **User Interaction**: Allows regeneration of failed steps or holding the process. --- ### Detailed Analysis #### Full-Proof Strategy - **Flow**: Entire proof is processed as a single unit. Auto-formalization and verification occur in one pass. - **Outcomes**: Binary result (succeed/failed). No iterative refinement. #### Step-Proof Strategy - **Flow**: Step-by-step verification with incremental validation. - **Formal Proof Stack**: Tracks progress (green = verified, yellow = current step). - **Regenerate**: User can rework failed steps. - **Hold**: Pauses the process for manual intervention. - **Advantages**: Supports iterative refinement, reduces risk of catastrophic failure. --- ### Key Observations 1. **Color Coding**: - Green: Success/verified steps. - Red: Failed verification. - Yellow: Current step in progress. 2. **User Role**: Explicit in Step-Proof Strategy (regenerate/hold), absent in Full-Proof. 3. **QED**: Marks the end of proofs in both strategies. --- ### Interpretation The diagram highlights a trade-off between simplicity and flexibility: - **Full-Proof Strategy** is straightforward but rigid, suitable for proofs where errors are unlikely or easily corrected. - **Step-Proof Strategy** introduces complexity but enables incremental validation, critical for large or error-prone proofs. The Formal Proof Stack and user interaction mechanisms suggest a focus on robustness and adaptability. This aligns with principles of **Peircean abduction** (hypothesis testing) and **incremental verification** in formal methods, emphasizing iterative refinement over monolithic validation. </details> Figure 1: Full-Proof Strategy generate from the whole proof and only provide proof result instead of detailed feedback to help user improve the proof. While Step-Proof separate the whole proof into sub-proof to proof from the bottom to the top and enable the user to get more detailed feedback and fine-grained operation. First, in the FULL-PROOF automated formalization process, the highly structured and formalized nature of the input and output, coupled with the numerous similarities in solving mathematical equations, often leads to excessive noise in the output. To obtain the desired formalized content, numerous filters must be set up, which results in considerable waste and contamination of generated content. This can also cause generation loops, where the same content is repeatedly generated, a common issue in FULL-PROOF strategies. Additionally, the length of proofs varies, and LLMs in FULL-PROOF struggle to adjust the output’s max_new_tokens effectively based on input length. This leads to shorter proofs not being truncated in time, thus generating repetitive or noisy content, and longer proofs lacking sufficient max_new_tokens. Lastly, the stability of FULL-PROOF generation is poor. For instance, a full proof might be almost entirely correct except for a minor error in a small step, leading to the failure of the entire formal proof. Users attempting regeneration may find previously correct parts presenting erroneous. Thus, FULL-PROOF requires highly accurate one-time generation of the entire content. Moreover, the correlation between formal and informal content generated by FULL-PROOF is weak, making it difficult for users to map formal feedback to corresponding informal content. Although LLMs can generate formal proofs with annotations to map back to informal proofs as Qinghua et al proposed the failure step detection method in SlideRule, this approach is unstable in practice and increases the required token count. 3.2 STEP-PROOF <details> <summary>extracted/6582548/user_interface.png Details</summary>  ### Visual Description ## Screenshot: Step Proof Interface ### Overview The image shows a screenshot of a proof assistant interface titled "Step Proof." It displays a formal mathematical proof process, including a problem statement, proof steps, and UI elements for managing the proof. The interface uses a structured format with commands like `PROOF`, `HIDE`, `REGEN`, `HOLD`, and `UNDO` to guide the user through constructing a proof. ### Components/Axes - **Header**: - Title: "Step Proof" (centered at the top). - File menu (left-aligned). - Close (`X`), minimize (`-`), and maximize (`+`) buttons (right-aligned). - **Main Content**: - **Problem Statement**: - Text: "Let $a, b, n$ be integers. Prove that if $a | n$ and $b | n$ with $\gcd(a, b) = 1$ then $ab | n$." - Highlighted sections (green) emphasize key steps in the proof. - **Proof Steps**: - **Lemma 1**: - Text: "Since $a | n$, $n$ could be rewritten as $(n/a) * a$." - Command: `PROOF` (button labeled "PROOF"). - **Lemma 2**: - Text: "Therefore, $b | n$ is equal to $b | (n/a) * a$." - Command: `HIDE` (button labeled "HIDE"). - **Lemma 3**: - Text: "Since $\gcd(a, b) = 1$ and $b | (n/a) * a$, it means that $b | (n/a)$. By multiplying $a$ on both sides of $b | (n/a)$, we get $ab | n$." - Command: `REGEN` (button labeled "REGEN"). - **UI Elements**: - Buttons: `PROOF`, `HIDE`, `REGEN`, `HOLD`, `UNDO` (aligned horizontally). - Status bar: "Status: Proof has been completed." - **Footer**: - "QED" (centered at the bottom). ### Detailed Analysis - **Problem Statement**: The problem is a number theory statement about divisibility and coprimality. The goal is to prove that if two integers $a$ and $b$ both divide $n$ and are coprime ($\gcd(a, b) = 1$), then their product $ab$ also divides $n$. - **Proof Steps**: 1. **Lemma 1**: Rewrites $n$ as $(n/a) * a$ to express divisibility by $a$. 2. **Lemma 2**: Substitutes $n$ into the divisibility condition for $b$, showing $b | (n/a) * a$. 3. **Lemma 3**: Uses the coprimality condition ($\gcd(a, b) = 1$) to conclude $b | (n/a)$, then multiplies both sides by $a$ to derive $ab | n$. - **UI Commands**: - `PROOF`: Likely initiates a new proof step. - `HIDE`: Hides intermediate steps or assumptions. - `REGEN`: Regenerates or re-evaluates a step. - `HOLD`: Pauses or suspends a step. - `UNDO`: Reverts the last action. ### Key Observations - The proof is structured hierarchically, with each lemma building on the previous one. - The use of `$` symbols indicates LaTeX-style mathematical notation, common in formal proofs. - The status "Proof has been completed" suggests the interface automatically verifies the correctness of the steps. ### Interpretation This interface is designed for formal verification of mathematical proofs, likely in a domain like number theory or algebra. The step-by-step approach with commands (`PROOF`, `HIDE`, etc.) allows users to incrementally build and validate proofs, ensuring logical consistency. The completion status implies the system checks for errors or gaps in the reasoning, providing a robust tool for mathematicians or students. The highlighted sections in the problem statement emphasize critical steps, guiding the user through the proof process. **Note**: No numerical data or charts are present; the focus is on textual and structural elements of a formal proof. </details> Figure 2: User Interface of StepProof To address the numerous issues faced by the FULL-PROOF strategy, we innovatively propose STEP-PROOF. STEP-PROOF employs a step-by-step generation and verification strategy, offering better performance and stability compared to FULL-PROOF. The workflow of STEP-PROOF is illustrated in the right of Figure 1. Unlike the one-time generation and verification of FULL-PROOF, STEP-PROOF assumes each sentence in the proof is a verifiable sub-proposition. Each step is formalized and pushed onto a formal proof stack, where it is verified along with other sub-propositions in the stack. Upon successful verification, the formalized proof and informal proof are packaged as inputs for the next step. For failed steps, the Step Proof allows users to backtrack, retaining previously verified steps and only clearing the erroneous step from the stack. The StepProof can then either re-formalize or optimize the existing informal step as needed. STEP-PROOF offers several advantages over FULL-PROOF. First, it only needs to formalize single sentences in context, resulting in shorter, less noisy, and more stable output. The step-by-step generation strategy also means that each step’s length is relatively fixed, eliminating the need for adjusting max_new_tokens and allowing the use of smaller max_new_tokens for formalizing longer theorems. Moreover, STEP-PROOF’s incremental generation and verification tolerate step errors well. Only the specific erroneous step needs to be retracted, rather than regenerating the entire content, enhancing robustness and efficiency. Finally, Step Proof ensures high correspondence between each informal and formal proof step, providing users with finer operational granularity. For instance, users can suspend a correct but incomplete step and assume it is correct to proceed, a functionality almost impossible under the FULL-PROOF strategy. We also designed a simple and user-friendly interactive interface for the user, as shown in Figure 2. Users can complete the natural language proof of the problem through interface interaction, and each step of the proof will be formally verified after submission, and the verified proof step will be marked in green in the background to indicate that the current step has passed the verification and is reliable. If the current step does not pass the automatic validation but the user thinks it is true and wants to continue, you can select HOLD, and the current step will be highlighted in yellow in the background to indicate that the current step is in a suspended state. After completing all the proof steps, the user can input QED to indicate that the system has completed the proof, and the system will combine all the steps to perform the final verification of the proof target. Through the interactive interface, the user can also realize the PDF export of the proof process. 4 Experiment 4.1 Experiment Setup To validate the performance advantages of the STEP-PROOF strategy over FULL-PROOF, and to compare StepProof’s overall performance against existing automated formal proof methods, we conducted both strategy performance tests and baseline tests using the same dataset and model settings. For the test dataset, we used GSM8K, which includes a large number of informal mathematical problems and their correct informal proofs. These informal proofs can be easily segmented into a series of sub-steps. We chose Llama3 8B-Instruct as the large language model for automated formalization. Existing autoformalization tests use closed-source models, and we aim to fill this gap by using an open-source small LLMs. We set the temperature to 0.3 to balance stability and flexibility. Given the small parameter count of 8B, we used a single example for the few-shot in strategy performance tests. With proof steps in GSM8K (cobbe2021gsm8k, ) averaging 4-5 steps, we set the max_new_tokens for FULL-PROOF to 1024, and 256 for each step in Step Proof. The test environment consisted of a single NVIDIA A4000 16GB, 8 cores of AMD5800X, and 32GB DDR4 3200 RAM. Isabelle2024 was used as the formal theorem prover with only Main prove library as the theorem base Here, we only use Main as the proof library, considering that the use of different libraries will greatly affect the formal verification ability of the theorem prover, in order to provide a relatively standard index. In StepProof, we do not introduce other libraries to further improve the proof ability of the theorem prover. Introducing more libraries in practice will greatly improve the proof ability of the theorem prover, and also improve the proof ability of the whole system to some extent., with Isabelle-client (shminke2022python, ) as the testing service proxy. In the strategy performance tests, we evaluated the performance of FULL-PROOF and STEP-PROOF on the GSM8K test set using the following metrics: 1. One-attempt generation proof pass rate $r_{p}$ . 2. Average formalization time for passed proofs $\mu_{f}$ . 3. Variance in formalization time $\sigma_{f}^{2}$ . 4. Average proof time for passed proofs $\mu_{p}$ . 5. Variance in proof time $\sigma_{p}^{2}$ . In the baseline tests, we compared the multi-attempt test results of GSM8K by Lewkowycz et al. (lewkowycz2022solvingquantitativereasoningproblems, ) in Majority Voting and Zhou et al. (zhou2024don, ) in DTV with our results. We evaluated the performance based on the number of attempts and multi-round proof pass rate, allowing up to 10 retries for each failed step in each formalization attempt. At the same time, considering that StepProof has better granularity than traditional proof tasks, we not only evaluated the overall proof passing rate but also counted the proportion of step-proof passing. For example, if a 6-step proofs can be verified to be true in 3 steps, then we will mark that the step pass rate of the proof is 0.5. In this way, we quantify the formal proof capability of the method more comprehensively rather than the Proof Passing Rate. In addition, to verify the influence of the writing method of non-formal proof on the passing rate of StepProof formal proof, we extracted 100 questions from the Number theory of MATH (hendrycksmath2021, ) and made simple manual modifications to make the proof step more consistent with the proof requirement of StepProof. 4.2 Experiment Results | | Proof Passing Rate $r_{p}$ | Formalization Time $\mu_{f}±\sigma_{f}^{2}$ | Proof Time $\mu_{p}±\sigma_{p}^{2}$ | | --- | --- | --- | --- | | FULL-PROOF | 5.30% | 9.54 ± 12.64s | 214.93 ± 20864.97s | | STEP-PROOF | 6.10% | 5.83 ± 4.24s | 130.12 ± 5271.65s | Table 1: Performance Test of Full-Proof and Step-Proof In strategy performance tests, the STEP-PROOF strategy outperformed the FULL-PROOF strategy across the board on the GSM8K test set. As shown in Table 1, the STEP-PROOF strategy improved the one-attempt proof pass rate by 15.1% compared to FULL-PROOF. In terms of average formalization time, STEP-PROOF required 38.9% less time than FULL-PROOF. For average proof time, STEP-PROOF achieved a 39.5% performance improvement over FULL-PROOF. Additionally, STEP-PROOF showed more stability in both formalization and proof time compared to FULL-PROOF. These results confirm that our strategy offers better performance, efficiency and stability. | Majority Voting Don’t Trust:Verify* StepProof | 64 64 10 | 16.2% 25.3% 22.0% | - 31.3% 100% | Minerva 8B Llama3 8B GLM4 9B(4bit) | | --- | --- | --- | --- | --- | | StepProof | 10 | 27.9% | 100% | Llama3 8B | Table 2: Baseline Test in GSM8K In the baseline test as shown in Table 2, Step Proof surpassed DTV in multi-round verification tests on GSM8K, achieving a 10.3% performance improvement. Moreover, StepProof required fewer attempts compared to DTV Don’t Trust: Verify (DTV) originally used two close source models–GPT3.5 as the problem generation model and Minerva 8B as the proof generation model, while due to the Minerva being inaccessible and GPT3.5 being costing, we use the same method in DTV, but replace the LLM into Llama3., demonstrating its superior proof capability and further validating the advantages of the StepProof methods. | $0=r_{s}$ $0<r_{s}$ $0.5≤ r_{s}$ | 79.6% 20.4% 14.6% | 50.5% 49.5% 38.1% | 83.9% 16.1% 13.4% | 55.4% 44.6% 41.9% | | --- | --- | --- | --- | --- | | $1=r_{s}$ | 6.1% | 27.9% | 4.8% | 22.0% | Table 3: Step Passing Rate Distribution in GSM8K In the step pass rate test as shown in Table 3, we found that StepProof was able to perform some degree of validation for nearly half of the proofs after 10 rounds of trying. In LLAMA3 8B, 38.1% of the proofs completed more than half of the verification, and 27.9% of the proofs completed all of the verification. Compared with a single attempt, this is a significant improvement. At the same time, we propose a new indicator-step passing rate ( $r_{s}$ ) for a more comprehensive evaluation of the proof of automatic formal verification methods. | $0=r_{s}$ $0<r_{s}$ $0.5≤ r_{s}$ | 35% 65% 42% | 32% 68% 45% | | --- | --- | --- | | $1=r_{s}$ | 6% | 12% | Table 4: Step Passing Rate Distribution in Number Theory In our test to verify the influence of informal proof writing on the proof pass rate (as shown in the Table 4), we found that the proof pass rate was significantly improved after simple fitting of the informal proof. This shows that compared with FULL-PROOF, STEP-PROOF adopts proof mathematics that is more suitable for step verification, which will be more conducive to improving the pass rate of automatic formal verification. 4.3 Experiment Analysis <details> <summary>extracted/6582548/Compare.png Details</summary>  ### Visual Description ## Scatter Plots: Formal and Proof Times of Two Strategies ### Overview The image contains two side-by-side scatter plots comparing the performance of two proof strategies ("Full Proof" and "Step Proof") across varying proof lengths (4–11). The left plot measures "Formal Time" (y-axis) and the right plot measures "Proof Time" (y-axis), both plotted against "Proof Length" (x-axis). Data points are color-coded: blue for Full Proof, green for Step Proof. --- ### Components/Axes #### Left Plot: Formal Times of Two Strategy - **X-axis (Proof Length)**: Discrete values from 4 to 11 (integer scale). - **Y-axis (Formal Time)**: Continuous scale from 0 to 25. - **Legend**: - Blue dots = Full Proof - Green dots = Step Proof - **Title**: "Formal Times of Two Strategy" #### Right Plot: Proof Times of Two Strategy - **X-axis (Proof Length)**: Same as left plot (4–11). - **Y-axis (Proof Time)**: Continuous scale from 0 to 700. - **Legend**: Identical to left plot (blue = Full Proof, green = Step Proof). - **Title**: "Proof Times of Two Strategy" --- ### Detailed Analysis #### Left Plot: Formal Time Trends - **Full Proof (Blue)**: - At Proof Length 4: Formal Time ≈ 12–15 (clustered around 12–15). - At Proof Length 6: Sharp peak at ~24 (highest value). - At Proof Length 8: Values drop to ~10–12. - At Proof Length 11: Lowest value (~7). - **Step Proof (Green)**: - Consistently lower than Full Proof across all lengths. - At Proof Length 9: Peaks at ~15 (highest for Step Proof). - At Proof Length 11: Drops to ~5. #### Right Plot: Proof Time Trends - **Full Proof (Blue)**: - At Proof Length 4: ~300–400. - At Proof Length 8: Peaks at ~700 (highest value). - At Proof Length 11: Drops to ~100. - **Step Proof (Green)**: - At Proof Length 4: ~200–250. - At Proof Length 8: ~200 (lower than Full Proof). - At Proof Length 11: ~50 (lowest value). --- ### Key Observations 1. **Inverse Relationship**: Both strategies show decreasing times as Proof Length increases, but Full Proof exhibits higher variability. 2. **Peak at Length 8**: Full Proof reaches its maximum Proof Time (~700) at Proof Length 8, while Step Proof remains stable. 3. **Efficiency Gap**: Step Proof consistently requires less time than Full Proof (e.g., at Proof Length 11, Step Proof is ~50 vs. Full Proof’s ~100). 4. **Outlier at Length 6**: Full Proof’s Formal Time spikes to ~24, far exceeding other lengths. --- ### Interpretation - **Efficiency of Step Proof**: Step Proof demonstrates superior efficiency, requiring significantly less time across all proof lengths. This suggests it may be preferable for practical applications. - **Full Proof’s Scalability**: Despite higher resource consumption, Full Proof’s time decreases with longer proofs, potentially indicating better handling of complex cases. - **Anomaly at Length 6**: The spike in Formal Time for Full Proof at Proof Length 6 warrants investigation—could reflect computational bottlenecks or edge-case handling. The data implies a trade-off: Step Proof optimizes speed, while Full Proof may offer robustness for longer proofs at the cost of higher resource usage. </details> Figure 3: Time Cost of Two Strategies in Formalization and Proof From Figure 3, we find that compared with the FULL-PROOF Strategy, STEP-PROOF takes less time to formalize and prove and is more stable. On the one hand, the generation strategy of Step-Proof makes the content generated in a single attempt less and more stable. Stable step content reduces the number of false proofs and the time to repeatedly prove successful content. Therefore, in terms of both generation efficiency and proof efficiency, STEP-PROOF is superior to FULL-PROOF. <details> <summary>extracted/6582548/Attempts.png Details</summary>  ### Visual Description ## Bar Charts: Passed Proofs and Step Proofs in Different Attempts ### Overview The image contains two side-by-side bar charts comparing the performance of two AI models, **LLAMA3 8B** (blue) and **GLM4 9B (4bit)** (green), across 10 attempts. The left chart measures "Passed Proofs," while the right chart measures "Passed Step Proofs." Both charts show a decline in performance as the number of attempts increases. ### Components/Axes #### Left Chart: Passed Proofs in Different Attempts - **X-axis (Attempts)**: Labeled "Attempts," with discrete categories from 1 to 10. - **Y-axis (Passed Proofs)**: Labeled "Passed Proofs," with a linear scale from 0 to 140. - **Legend**: Located at the top-right corner, associating blue with LLAMA3 8B and green with GLM4 9B (4bit). #### Right Chart: Passed Step Proofs in Different Attempts - **X-axis (Attempts)**: Same as the left chart (1–10). - **Y-axis (Passed Step Proofs)**: Labeled "Passed Step Proofs," with a linear scale from 0 to 4,500. - **Legend**: Identical to the left chart, with blue for LLAMA3 8B and green for GLM4 9B (4bit). ### Detailed Analysis #### Left Chart: Passed Proofs - **LLAMA3 8B (Blue)**: - Attempt 1: ~130 - Attempt 2: ~55 - Attempt 3: ~40 - Attempt 4: ~30 - Attempt 5: ~25 - Attempt 6: ~20 - Attempt 7: ~18 - Attempt 8: ~12 - Attempt 9: ~10 - Attempt 10: ~15 - **GLM4 9B (4bit) (Green)**: - Attempt 1: ~65 - Attempt 2: ~45 - Attempt 3: ~38 - Attempt 4: ~28 - Attempt 5: ~22 - Attempt 6: ~20 - Attempt 7: ~12 - Attempt 8: ~15 - Attempt 9: ~20 - Attempt 10: ~20 #### Right Chart: Passed Step Proofs - **LLAMA3 8B (Blue)**: - Attempt 1: ~4,400 - Attempt 2: ~1,200 - Attempt 3: ~300 - Attempt 4: ~100 - Attempt 5: ~50 - Attempt 6: ~30 - Attempt 7: ~10 - Attempt 8: ~5 - Attempt 9: ~2 - Attempt 10: ~1 - **GLM4 9B (4bit) (Green)**: - Attempt 1: ~4,300 - Attempt 2: ~1,400 - Attempt 3: ~600 - Attempt 4: ~200 - Attempt 5: ~100 - Attempt 6: ~50 - Attempt 7: ~30 - Attempt 8: ~15 - Attempt 9: ~5 - Attempt 10: ~2 ### Key Observations 1. **Decline in Performance**: Both models show a consistent decline in passed proofs and step proofs as attempts increase. 2. **LLAMA3 8B Dominance**: LLAMA3 8B outperforms GLM4 9B (4bit) in both metrics, particularly in the first attempt. 3. **Step Proofs Scale**: The right chart’s y-axis spans a much larger range (0–4,500), suggesting step proofs are a more granular or cumulative metric. 4. **GLM4 Resilience**: GLM4 9B (4bit) shows a slower decline in passed proofs compared to LLAMA3 8B, though it remains consistently lower. ### Interpretation - **Model Efficiency**: LLAMA3 8B achieves higher initial success but degrades faster with repeated attempts, possibly due to overfitting or resource constraints. - **GLM4 Trade-off**: GLM4 9B (4bit) sacrifices initial performance for more sustained results, indicating better generalization or efficiency in later attempts. - **Step Proofs Complexity**: The drastic drop in step proofs (right chart) suggests that later attempts involve increasingly complex or interdependent tasks, where both models struggle. - **Anomaly in Attempt 10**: GLM4 9B (4bit) shows a slight uptick in passed proofs at attempt 10, which may indicate a recovery phase or data inconsistency. This analysis highlights trade-offs between initial performance and long-term reliability, with implications for model selection depending on task requirements. </details> Figure 4: Passed Proofs and Steps in Different Attempts To investigate the relation between step proof pass rate and number of attempts, we plotted Figure 4. It shows that most steps can be proven with relatively few attempts, with only a small fraction requiring multiple tries. We believe the main limitation to step pass rate lies not in the model’s formalization ability, but in whether the informal proof steps are suitable for conversion into provable formal steps. We found that many steps in the test set cannot be formalized into provable steps. These unformalizable informal steps significantly limit the further performance improvement of Step Proof. Therefore, to better achieve verification in practical applications of StepProof, each proof sub-step should be ensured to be a formally verifiable sub-proposition as much as possible. In addition, we also found that the processing capacity of LLMs is poor when faced with the processing of continuous equations, and it is easy to fall into the generation loop during the generation process, resulting in the poor quality of the generated formal proof. Therefore, in practical applications, it is necessary to split the steps as much as possible, rather than pursue once completion. At the same time, since the automatic proof ability of automated theorem proving is also limited, resolving the proof process is not only conducive to the formalization process, but also very helpful to the verification process. 5 Limitations & Future Research At present, the performance of StepProof in small models has been verified in various aspects. However, due to the lack of equipment and funds, the performance of StepProof in larger models has not been verified, although the previous relevant work verified the conclusion that FULL-PROOF strategy has better performance in larger models. However, the STEP-PROOF strategy has not yet been tested on a larger model. In addition, StepProof is strict for users to enter proof steps, while FULL-PROOF is more flexible and can incorporate some non-proof explanatory language or prompt words into the proof. However, StepProof will make mistakes in the step proof because the prompt word is not provable. Finally, StepProof pays more attention to the sequential proof with steps, but when faced with some structured proof methods, its performance is still limited, while FULL-PROOF can better capture the overall proof structure. In the future, our work will mainly start from the following two points: 1. At present, we are writing a corpus for StepProof for automatic formal verification tasks oriented to step verification, and we hope that a more targeted corpus will help improve the step formalization ability of the model. 2. We will implement specific structured proof based on the structured design of the system to further improve the integrity and flexibility of StepProof proof. 6 Conclusion In this paper, we innovatively propose a new automatic formal proof method called StepProof. StepProof implements sentence-level formal verification of natural language mathematical proofs, allowing users to conduct more flexible formal verification. At the same time, compared with the traditional FullProof strategy, StepProof has been significantly improved in formalization, proof efficiency and proof accuracy. In addition, StepProof can preserve the contents of the proof that has already been verified, providing more information than the traditional Full-Proof strategy that can only indicate the passage and failure of the proof. We used a small model on the GSM8K data set to test the proof pass rate, and its performance reached the level of state-of-the-art. We also conducted a test on the Number Theory dataset of MATH to test the effect of formal content writing on the proof pass rate. The experimental results show that by optimizing the non-formal proof for step verification, the passing rate of the non-formal proof can be significantly improved. We will further optimize the architecture of StepProof in future work to make it more flexible to handle formal verification of various non-formal mathematical proofs. References - [1] John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg H. Siekmann, editor, Computational Logic, volume 9 of Handbook of the History of Logic, pages 135–214. North-Holland, 2014. - [2] Filip Maric. A survey of interactive theorem proving. Zbornik radova, 18(26):173–223, 2015. - [3] M Saqib Nawaz, Moin Malik, Yi Li, Meng Sun, and M Lali. A survey on theorem provers in formal methods. arXiv preprint arXiv:1912.03028, 2019. - [4] Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, et al. A survey of large language models. arXiv preprint arXiv:2303.18223, 2023. - [5] Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing. ACM Computing Surveys, 55(9):1–35, 2023. - [6] Yaqing Wang, Quanming Yao, James T Kwok, and Lionel M Ni. Generalizing from a few examples: A survey on few-shot learning. ACM computing surveys (csur), 53(3):1–34, 2020. - [7] Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023. - [8] Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Ye Jin Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. ACM Computing Surveys, 55(12):1–38, 2023. - [9] Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Wei Yu, Xinying Song, and Denny Zhou. Large language models cannot self-correct reasoning yet. arXiv preprint arXiv:2310.01798, 2023. - [10] Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024. - [11] Andrea Asperti. A survey on interactive theorem proving. URL: http://www. cs. unibo. it/~ asperti/SLIDES/itp. pdf, 2009. - [12] John Harrison. A survey of automated theorem proving. Sat, 17:20–18, 2013. - [13] Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. - [14] Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178, 1997. - [15] Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer, 2015. - [16] Artem Yushkovskiy. Comparison of two theorem provers: Isabelle/hol and coq. arXiv preprint arXiv:1808.09701, 2018. - [17] Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024. - [18] Junjie Ye, Xuanting Chen, Nuo Xu, Can Zu, Zekai Shao, Shichun Liu, Yuhan Cui, Zeyang Zhou, Chao Gong, Yang Shen, et al. A comprehensive capability analysis of gpt-3 and gpt-3.5 series models. arXiv preprint arXiv:2303.10420, 2023. - [19] Team GLM, Aohan Zeng, Bin Xu, Bowen Wang, Chenhui Zhang, Da Yin, Diego Rojas, Guanyu Feng, Hanlin Zhao, Hanyu Lai, Hao Yu, Hongning Wang, Jiadai Sun, Jiajie Zhang, Jiale Cheng, Jiayi Gui, Jie Tang, Jing Zhang, Juanzi Li, Lei Zhao, Lindong Wu, Lucen Zhong, Mingdao Liu, Minlie Huang, Peng Zhang, Qinkai Zheng, Rui Lu, Shuaiqi Duan, Shudan Zhang, Shulin Cao, Shuxun Yang, Weng Lam Tam, Wenyi Zhao, Xiao Liu, Xiao Xia, Xiaohan Zhang, Xiaotao Gu, Xin Lv, Xinghan Liu, Xinyi Liu, Xinyue Yang, Xixuan Song, Xunkai Zhang, Yifan An, Yifan Xu, Yilin Niu, Yuantao Yang, Yueyan Li, Yushi Bai, Yuxiao Dong, Zehan Qi, Zhaoyu Wang, Zhen Yang, Zhengxiao Du, Zhenyu Hou, and Zihan Wang. Chatglm: A family of large language models from glm-130b to glm-4 all tools, 2024. - [20] Junbing Yan, Chengyu Wang, Jun Huang, and Wei Zhang. Do large language models understand logic or just mimick context? arXiv preprint arXiv:2402.12091, 2024. - [21] Yuxuan Wan, Wenxuan Wang, Yiliu Yang, Youliang Yuan, Jen-tse Huang, Pinjia He, Wenxiang Jiao, and Michael R Lyu. A & b== b & a: Triggering logical reasoning failures in large language models. arXiv preprint arXiv:2401.00757, 2024. - [22] Shalom Lappin. Assessing the strengths and weaknesses of large language models. Journal of Logic, Language and Information, 33(1):9–20, 2024. - [23] Wenqi Fan, Yujuan Ding, Liangbo Ning, Shijie Wang, Hengyun Li, Dawei Yin, Tat-Seng Chua, and Qing Li. A survey on rag meeting llms: Towards retrieval-augmented large language models. In Proceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, pages 6491–6501, 2024. - [24] Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824–24837, 2022. - [25] Tushar Khot, Harsh Trivedi, Matthew Finlayson, Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. Decomposed prompting: A modular approach for solving complex tasks. arXiv preprint arXiv:2210.02406, 2022. - [26] Thien Huu Nguyen and Ralph Grishman. Relation extraction: Perspective from convolutional neural networks. In Proceedings of the 1st workshop on vector space modeling for natural language processing, pages 39–48, 2015. - [27] Hrituraj Singh, Milan Aggrawal, and Balaji Krishnamurthy. Exploring neural models for parsing natural language into first-order logic. arXiv preprint arXiv:2002.06544, 2020. - [28] Xuantao Lu, Jingping Liu, Zhouhong Gu, Hanwen Tong, Chenhao Xie, Junyang Huang, Yanghua Xiao, and Wenguang Wang. Parsing natural language into propositional and first-order logic with dual reinforcement learning. In Proceedings of the 29th International Conference on Computational Linguistics, pages 5419–5431, 2022. - [29] Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 85–98, 2020. - [30] Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models, 2022. - [31] Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022. - [32] Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. arXiv preprint arXiv:2403.18120, 2024. - [33] Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023. - [34] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021. - [35] Boris Shminke. Python client for isabelle server. arXiv preprint arXiv:2212.11173, 2022. - [36] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. NeurIPS, 2021. - [37] Mohammadreza Pourreza and Davood Rafiei. Din-sql: Decomposed in-context learning of text-to-sql with self-correction. Advances in Neural Information Processing Systems, 36, 2024. Appendix A Appendix A.1 Additional Case of Manual Modification for Step Proof Fitting For the following informal problem and proof: Problem: What is the average of the two smallest positive integer solutions to the congruence $14u\equiv 46±od{100}$ . Show it is 64. Solution: Note that $14$ , $46$ , and $100$ all have a common factor of $2$ , so we can divide it out: the solutions to $$ 14u\equiv 46\pmod{100} $$ are identical to the solutions to $$ 7u\equiv 23\pmod{50}. $$ Make sure you see why this is the case. Now we can multiply both sides of the congruence by $7$ to obtain $$ 49u\equiv 161\pmod{50}, $$ which also has the same solutions as the previous congruence, since we could reverse the step above by multiplying both sides by $7^{-1}$ . (We know that $7^{-1}$ exists modulo $50$ because $7$ and $50$ are relatively prime.) Replacing each side of $49u\equiv 161$ by a $±od{50}$ equivalent, we have $$ -u\equiv 11\pmod{50}, $$ and thus $$ u\equiv-11\pmod{50}. $$ This is the set of solutions to our original congruence. The two smallest positive solutions are $-11+50=39$ and $-11+2· 50=89$ . Their average is $\boxed{64}$ . In normal cases, we can cut the content according to the period to get the following sequence of non-formal proofs. ⬇ 1 Note that $14$, $46$, and $100$ all have a common factor of $2$, so we can divide it out: the solutions to $$14u \ equiv 46 \ pmod {100} $$ are identical to the solutions to $$7u \ equiv 23 \ pmod {50}. $$ 2 3 Make sure you see why this is the case. 4 5 Now we can multiply both sides of the congruence by $7$ to obtain $$49u \ equiv 161 \ pmod {50}, $$ which also has the same solutions as the previous congruence, since we could reverse the step above by multiplying both sides by $7 ^{-1} $. 6 7 We know that $7 ^{-1} $ exists modulo $50$ because $7$ and $50$ are relatively prime. 8 9 Replacing each side of $49u \ equiv 161 $ by a $ \ pmod {50} $ equivalent, we have $$ - u \ equiv 11\ pmod {50}, $$ and thus $$u \ equiv -11\ pmod {50}. $$ 10 11 This is the set of solutions to our original congruence. 12 13 The two smallest positive solutions are $ -11+50 = 39 $ and $ -11+2\ cdot 50 = 89 $. 14 15 Their average is $ \ boxed {64} $. However, there are many problems with such a simple decomposition. Such as the following sentences are unable to be formalized. ⬇ 1 Make sure you see why this is the case. 2 3 This is the set of solutions to our original congruence. In addition, from the point of view of the order of proof, I can see that " We know that $7^{-1}$ exists modulo $50$ because $7$ and $50$ are relatively prime. " is a prerequisite for " Now we can multiply both sides of the congruence by $7$ to obtain $49u\equiv 161±od{50}$ , which also has the same solutions as the previous congruence, since we could reverse the step above by multiplying both sides by $7^{-1}$ . ", so the order of the two should be reversed. Therefore, in order to meet the requirements of StepProof, I deleted the statements that could not be formalized and corrected the sequence to obtain the following proof sequence. ⬇ 1 Note that $14$, $46$, and $100$ all have a common factor of $2$, so we can divide it out: the solutions to $$14u \ equiv 46 \ pmod {100} $$ are identical to the solutions to $$7u \ equiv 23 \ pmod {50}. $$ 2 3 We know that $7 ^{-1} $ exists modulo $50$ because $7$ and $50$ are relatively prime. 4 5 Now we can multiply both sides of the congruence by $7$ to obtain $$49u \ equiv 161 \ pmod {50}, $$ which also has the same solutions as the previous congruence, since we could reverse the step above by multiplying both sides by $7 ^{-1} $. 6 7 Replacing each side of $49u \ equiv 161 $ by a $ \ pmod {50} $ equivalent, we have $$ - u \ equiv 11\ pmod {50}, $$ and thus $$u \ equiv -11\ pmod {50}. $$ This is the set of solutions to our original congruence. 8 9 The two smallest positive solutions are $ -11+50 = 39 $ and $ -11+2\ cdot 50 = 89 $. 10 11 Their average is $ \ boxed {64} $. A.2 Formal Content Comparison between Full-Proof and Step-Proof Problem: Given that $1<x<2$ , show that $\sqrt{(x-1)^{2}}+|x-2|$ can be reduced to 1. Solution: Since $x>1$ , we know that $\sqrt{(x-1)^{2}}=x-1$ . And since $x<2$ , we know that $|x-2|=2-x$ . Therefore, it can be rewritten as $x-1+2-x$ , and we know that it can be reduced to 1. After formalize the problem we get following Isabelle statement. ⬇ 1 theorem sqrt_abs_simplify: 2 assumes h0: "1 < x " 3 and h1: " x < 2" 4 shows " sqrt ((x - 1)^2) + abs (x - 2) = 1" Using Full-Proof, we can directly obtain the following formal proof. ⬇ 1 proof - 2 have h2: " sqrt ((x - 1)^2) = x - 1" 3 using h0 by (simp add: abs_of_nonneg) 4 have h3: " abs (x - 2) = 2 - x " 5 using h1 by (simp add: abs_of_nonpos) 6 have " sqrt ((x - 1)^2) + abs (x - 2) = (x - 1) + (2 - x)" 7 using h2 h3 by simp 8 also have "... = 1" 9 by simp 10 finally show ? thesis . 11 qed In the StepProof approach, we would firstly input the first step ⬇ 1 Since $x > 1 $, we know that $ \ sqrt {(x -1)^2} = x - 1 $. Then after formalization, we can get corresponding formal proof. ⬇ 1 have h2: " sqrt ((x - 1)^2) = x - 1" using h0 by simp After this formal step has been verified, we will input the next steps in the same way. ⬇ 1 And since $x < 2 $, we know that $ | x -2| = 2- x$. ⬇ 1 have h3: " abs (x - 2) = 2 - x " using h1 by simp ⬇ 1 Therefore, it can be rewritten as $x - 1 + 2 - x$, and we know that it can be reduced to 1. ⬇ 1 show ? thesis using h2 h3 by simp After the global goal has been proven, the system will automatically align the formal proof with the informal proof. Then we will get the over all formal proof of StepProof as following ⬇ 1 proof - 2 (* Since $x > 1 $, we know that $ \ sqrt {(x -1)^2} = x - 1 $.*) 3 have h2: " sqrt ((x - 1)^2) = x - 1" using h0 by simp 4 (* And since $x < 2 $, we know that $ | x -2| = 2- x$.*) 5 have h3: " abs (x - 2) = 2 - x " using h1 by simp 6 (* Therefore, it can be rewritten as $x - 1 + 2 - x$, and we know that it can be reduced to 1.*) 7 show ? thesis using h2 h3 by simp 8 9 qed