Download PDFOpen PDF in browser

Assimilating the Structure of Formal and Informal Proof

EasyChair Preprint 6267

5 pagesDate: August 10, 2021

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser