Download PDFOpen PDF in browserAssimilating the Structure of Formal and Informal ProofEasyChair Preprint 62675 pages•Date: August 10, 2021AbstractFormal proof is regarded as an insufficient alternative to informal proof because it has both advantages and disadvantages, compared to informal proof. Focusing on the macro structure of proof, this study proposes assimilating the structure of formal proof and informal proof to retain both readability and verifiability. An implementation example of the Ntac system, a library for the Lean theorem prover, is introduced. The system converts Lean script into natural language text, which allows treating formal proof as informal proof. Keyphrases: formal proof, informal proof, natural language, structure
|