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: Full-Proof vs. Step-Proof Strategies ### Overview The image presents two diagrams illustrating different strategies for mathematical proof verification: a "Full-Proof Strategy" on the left and a "Step-Proof Strategy" on the right. Both strategies involve converting natural language math proofs into a formal representation and then checking their validity. The Step-Proof strategy includes a user interaction loop. ### Components/Axes **Full-Proof Strategy (Left Side):** * **Natural Language Math Proofs:** Labeled as "Step1, Step2, Step3, ..., QED" with a blue background. * **Auto-Formalization:** A rectangular box representing the process of converting natural language proofs into a formal representation. * **Checker:** A rectangular box representing the process of verifying the formal proof. * **Failed:** A red rectangle indicating a failed verification. * **Succeed:** A green rectangle indicating a successful verification. **Step-Proof Strategy (Right Side):** * **Natural Language Math Proofs:** Labeled as "[Step1, Step2, Step3, ..., QED]" with a blue background. * **Auto-Formalization:** A rectangular box representing the process of converting natural language proofs into a formal representation. * **Checker:** A rectangular box representing the process of verifying the formal proof. * **User:** A rectangular box representing user interaction. * **Formal Proof Stack:** A stack of blocks representing the formal proof steps. The top block is labeled "QED" and is green. The third block from the top is labeled "Formal Step 3" and is yellow. The bottom two blocks are labeled "Formal Step 1" and "Formal Step 2" and are green. * **Verified:** An arrow from the Checker to the Formal Proof Stack. * **Failed:** An arrow from the Checker to the User. * **Regenerate:** An arrow from the User to the Auto-Formalization. * **Hold:** An arrow from the User to the Checker. ### Detailed Analysis or ### Content Details **Full-Proof Strategy:** 1. Natural Language Math Proofs are fed into the Auto-Formalization process. 2. The output of Auto-Formalization is passed to the Checker. 3. The Checker either outputs "failed" (red) or "succeed" (green). **Step-Proof Strategy:** 1. Natural Language Math Proofs are fed into the Auto-Formalization process. 2. The output of Auto-Formalization is passed to the Checker. 3. If the Checker verifies a step, it is added to the Formal Proof Stack. 4. If the Checker fails, the User can either regenerate the proof or hold the current state. 5. The process continues until the Formal Proof Stack reaches "QED". ### Key Observations * The Full-Proof Strategy is a linear process, while the Step-Proof Strategy involves a loop with user interaction. * The Formal Proof Stack in the Step-Proof Strategy visually represents the progress of the proof. * The colors (red and green) indicate success or failure in the Full-Proof Strategy. ### Interpretation The diagrams illustrate two different approaches to automated proof verification. The Full-Proof Strategy attempts to verify the entire proof at once, while the Step-Proof Strategy breaks the proof into smaller steps and allows for user intervention if a step fails. The Step-Proof Strategy is likely more robust and adaptable, as it allows for human guidance in cases where the automated checker is unable to verify a step. The use of a "Formal Proof Stack" in the Step-Proof Strategy provides a visual representation of the proof's progress, which can be helpful for both the user and the system. </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 Application ### Overview The image is a screenshot of a "Step Proof" application, likely used for mathematical proofs. It shows a problem statement, a series of proof steps, and controls for manipulating the proof. The application appears to be in a desktop environment. ### Components/Axes * **Title Bar:** "Step Proof" * **Menu Bar:** "File" * **Problem Statement:** * "Let $a, b, n$ be integers. Prove that if $a | n$ and $b | n$ with $gcd(a, b) = 1$ then $ab | n$." * **Upload Problem Button:** "Upload Problem" * **Proofs Section:** Displays the steps of the proof. * **Add Proof Section:** Allows adding new steps to the proof. * **Status Bar:** "Status: Proof has been completed." * **Buttons:** "PROOF", "HIDE", "REGEN", "HOLD", "UNDO" (repeated for each proof step) ### Detailed Analysis or ### Content Details **Problem Statement:** * "Let $a, b, n$ be integers. Prove that if $a | n$ and $b | n$ with $gcd(a, b) = 1$ then $ab | n$." **Proofs Section:** * "PROBLEM: Let $a, b, n$ be integers. Prove that if $a | n$ and $b | n$ with $gcd(a, b) = 1$ then $ab | n$." * "PROOFS:" * "Since $a|n$, $n$ could be rewritten as $(n/a)*a$." (Highlighted in green) * "Therefore, $b|n$ is equal to $b|(n/a)*a$." (Highlighted in green) * "Since $gcd(a,b)=1$ and $b|(n/a)*a$, it means that $b|(n/a)$." (Highlighted in green) * "By multiple $a$ on the both side of $b|(n/a)$, we will know that $b*a|(n/a)*a$ and we can get $a*b|n$." (Highlighted in green) * "QED" **Add Proof Section:** * "Add Proof" * "Since $a|n$, $n$ could be rewritten as $(n/a)*a$. have h1: "n = n div a * a" using assms(1) sledgehammer" * "Therefore, $b|n$ is equal to $b|(n/a)*a$. have h2: "b dvd n div a * a" using assms(2) sledgehammer" * "Since $gcd(a,b)=1$ and $b|(n/a)*a$, it means that $b|(n/a)$. have h3: "b dvd n div a" using assms(3) h2 sledgehammer" * "By multiple $a$ on the both side of $b|(n/a)$, we will know that $b*a|(n/a)*a$ and we can get $a*b|n$. have h4: "a * b dvd n" using h3 sledgehammer" * "QED then show ?thesis by auto" **Buttons:** * Each proof step has the following buttons: "PROOF", "HIDE", "REGEN", "HOLD", "UNDO" **Status Bar:** * "Status: Proof has been completed." ### Key Observations * The application is designed to assist in constructing mathematical proofs. * The proof steps are displayed sequentially. * The "Add Proof" section allows users to add new steps to the proof. * The "PROOF", "HIDE", "REGEN", "HOLD", and "UNDO" buttons provide control over each step. * The status bar indicates that the proof has been completed. * The green highlighting indicates the current focus or selection within the proof. ### Interpretation The screenshot demonstrates a user interface for a mathematical proof assistant. The application guides the user through the steps required to prove a given theorem. The "Add Proof" section allows the user to incrementally build the proof, while the buttons provide control over each step. The highlighting suggests that the application may be interactive, allowing the user to select and manipulate different parts of the proof. The completed status indicates a successful proof construction. The application uses formal mathematical notation and terminology, suggesting it is intended for users with a background in mathematics. The use of "sledgehammer" suggests an automated proof assistant is being used. ``` </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 scatter plots side-by-side. Both plots compare "Proof Length" on the x-axis against time metrics on the y-axis. The left plot shows "Formal Time" versus "Proof Length," while the right plot shows "Proof Time" versus "Proof Length." Each plot displays two data series: "Full Proof" (blue) and "Step Proof" (green). ### Components/Axes **Left Plot: Formal Times of Two Strategy** * **Title:** Formal Times of Two Strategy * **X-axis:** * **Label:** Proof Length * **Scale:** 4 to 11, integer increments * **Y-axis:** * **Label:** Formal Time * **Scale:** 0 to 25, increments of 5 * **Legend:** Located in the top-right corner. * Blue dot: Full Proof * Green dot: Step Proof **Right Plot: Proof Times of Two Strategy** * **Title:** Proof Times of Two Strategy * **X-axis:** * **Label:** Proof Length * **Scale:** 4 to 11, integer increments * **Y-axis:** * **Label:** Proof Time * **Scale:** 0 to 700, increments of 100 * **Legend:** Located in the top-right corner. * Blue dot: Full Proof * Green dot: Step Proof ### Detailed Analysis **Left Plot: Formal Times of Two Strategy** * **Full Proof (Blue):** * At Proof Length 4: Formal Time ranges from approximately 7 to 12. * At Proof Length 5: Formal Time ranges from approximately 7 to 16. * At Proof Length 6: Formal Time ranges from approximately 7 to 10. * At Proof Length 7: Formal Time ranges from approximately 8 to 18. * At Proof Length 8: Formal Time ranges from approximately 7 to 19. * At Proof Length 9: Formal Time is approximately 7. * At Proof Length 10: No data points. * At Proof Length 11: No data points. * **Trend:** No clear trend. * **Step Proof (Green):** * At Proof Length 4: Formal Time ranges from approximately 3 to 11. * At Proof Length 5: Formal Time ranges from approximately 4 to 8. * At Proof Length 6: Formal Time ranges from approximately 5 to 9. * At Proof Length 7: Formal Time ranges from approximately 6 to 10. * At Proof Length 8: Formal Time ranges from approximately 7 to 10. * At Proof Length 9: Formal Time is approximately 16. * At Proof Length 10: Formal Time is approximately 8. * At Proof Length 11: No data points. * **Trend:** No clear trend. **Right Plot: Proof Times of Two Strategy** * **Full Proof (Blue):** * At Proof Length 4: Proof Time ranges from approximately 200 to 450. * At Proof Length 5: Proof Time ranges from approximately 200 to 570. * At Proof Length 6: Proof Time ranges from approximately 80 to 490. * At Proof Length 7: Proof Time ranges from approximately 200 to 350. * At Proof Length 8: Proof Time ranges from approximately 150 to 300. * At Proof Length 9: Proof Time ranges from approximately 200 to 250. * At Proof Length 10: Proof Time is approximately 410. * At Proof Length 11: Proof Time is approximately 110. * **Trend:** No clear trend. * **Step Proof (Green):** * At Proof Length 4: Proof Time ranges from approximately 10 to 250. * At Proof Length 5: Proof Time ranges from approximately 50 to 220. * At Proof Length 6: Proof Time ranges from approximately 50 to 200. * At Proof Length 7: Proof Time ranges from approximately 50 to 200. * At Proof Length 8: Proof Time ranges from approximately 50 to 150. * At Proof Length 9: Proof Time is approximately 210. * At Proof Length 10: Proof Time is approximately 240. * At Proof Length 11: No data points. * **Trend:** No clear trend. ### Key Observations * Both plots show a wide distribution of time values for each proof length, indicating variability in the time taken for both "Full Proof" and "Step Proof" strategies. * There are more data points for shorter proof lengths (4-8) than for longer proof lengths (9-11). * In the "Formal Time" plot, the "Full Proof" strategy appears to have some outliers with higher time values. * In the "Proof Time" plot, the "Full Proof" strategy generally has higher time values than the "Step Proof" strategy. ### Interpretation The scatter plots compare the performance of "Full Proof" and "Step Proof" strategies based on "Proof Length." The data suggests that the time taken for both strategies varies significantly for each proof length. The "Proof Time" plot indicates that "Full Proof" generally takes longer than "Step Proof." However, the absence of clear trends suggests that "Proof Length" alone is not a strong predictor of either "Formal Time" or "Proof Time." Other factors likely influence the time taken for each strategy. The data could be used to further investigate the relationship between proof strategy, proof length, and time taken, potentially identifying other variables that contribute to the observed variability. </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 Passed Step Proofs in Different Attempts ### Overview The image contains two bar charts side-by-side. Both charts compare the performance of two models, LLAMA3 8B and GLM4 9B (4bit), across different attempts. The left chart shows the number of "Passed Proofs," while the right chart shows the number of "Passed Step Proofs." The x-axis represents the attempt number (from 1 to 10), and the y-axis represents the count of proofs or step proofs. ### Components/Axes **Left Chart:** * **Title:** Passed Proofs in Different Attempts * **X-axis:** Attempts (labeled 1 to 10) * **Y-axis:** Passed Proofs (scale from 0 to 120) * **Legend:** * Blue: LLAMA3 8B * Green: GLM4 9B (4bit) **Right Chart:** * **Title:** Passed Step Proofs in Different Attempts * **X-axis:** Attempts (labeled 1 to 10) * **Y-axis:** Passed Step Proofs (scale from 0 to 4000) * **Legend:** * Blue: LLAMA3 8B * Green: GLM4 9B (4bit) ### Detailed Analysis **Left Chart (Passed Proofs):** * **LLAMA3 8B (Blue):** * Attempt 1: Approximately 128 * Attempt 2: Approximately 55 * Attempt 3: Approximately 40 * Attempt 4: Approximately 32 * Attempt 5: Approximately 27 * Attempt 6: Approximately 23 * Attempt 7: Approximately 22 * Attempt 8: Approximately 13 * Attempt 9: Approximately 12 * Attempt 10: Approximately 17 * Trend: Decreases sharply from attempt 1 to 2, then decreases gradually until attempt 9, then increases slightly at attempt 10. * **GLM4 9B (4bit) (Green):** * Attempt 1: Approximately 65 * Attempt 2: Approximately 48 * Attempt 3: Approximately 38 * Attempt 4: Approximately 29 * Attempt 5: Approximately 21 * Attempt 6: Approximately 21 * Attempt 7: Approximately 13 * Attempt 8: Approximately 12 * Attempt 9: Approximately 20 * Attempt 10: Approximately 20 * Trend: Decreases sharply from attempt 1 to 2, then decreases gradually until attempt 8, then increases slightly at attempts 9 and 10. **Right Chart (Passed Step Proofs):** * **LLAMA3 8B (Blue):** * Attempt 1: Approximately 4300 * Attempt 2: Approximately 300 * Attempt 3: Approximately 100 * Attempt 4: Approximately 50 * Attempt 5: Approximately 30 * Attempt 6: Approximately 20 * Attempt 7: Approximately 20 * Attempt 8: Approximately 15 * Attempt 9: Approximately 10 * Attempt 10: Approximately 10 * Trend: Decreases sharply from attempt 1 to 2, then decreases gradually until attempt 10. * **GLM4 9B (4bit) (Green):** * Attempt 1: Approximately 4350 * Attempt 2: Approximately 650 * Attempt 3: Approximately 250 * Attempt 4: Approximately 150 * Attempt 5: Approximately 50 * Attempt 6: Approximately 40 * Attempt 7: Approximately 30 * Attempt 8: Approximately 20 * Attempt 9: Approximately 15 * Attempt 10: Approximately 15 * Trend: Decreases sharply from attempt 1 to 2, then decreases gradually until attempt 10. ### Key Observations * In both charts, the number of passed proofs/step proofs decreases as the attempt number increases. * In the "Passed Proofs" chart, LLAMA3 8B generally outperforms GLM4 9B (4bit) across all attempts. * In the "Passed Step Proofs" chart, GLM4 9B (4bit) slightly outperforms LLAMA3 8B in the first attempt, but LLAMA3 8B generally outperforms GLM4 9B (4bit) across all attempts. * The most significant drop in performance occurs between the first and second attempts for both models in both charts. ### Interpretation The data suggests that both models are more successful in earlier attempts, with performance declining as the number of attempts increases. This could be due to the models learning from previous attempts and adjusting their strategies, or it could indicate that the task becomes more difficult with each subsequent attempt. LLAMA3 8B generally performs better than GLM4 9B (4bit) in terms of "Passed Proofs," while GLM4 9B (4bit) performs slightly better in the first attempt for "Passed Step Proofs." The sharp decline in performance between the first and second attempts highlights the importance of initial conditions or strategies in the success of these models. </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