Assimilating the Structure of Formal and Informal Proof

EasyChair Preprint 6267

Abstract

Formal 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

@booklet{EasyChair:6267,
  author    = {Kensho Tsurusaki and Akiko Aizawa},
  title     = {Assimilating the Structure of Formal and Informal Proof},
  howpublished = {EasyChair Preprint 6267},
  year      = {EasyChair, 2021}}