Download PDFOpen PDF in browser

Assimilating the Structure of Formal and Informal Proof

EasyChair Preprint no. 6267

5 pagesDate: August 10, 2021


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:
  author = {Kensho Tsurusaki and Akiko Aizawa},
  title = {Assimilating the Structure of Formal and Informal Proof},
  howpublished = {EasyChair Preprint no. 6267},

  year = {EasyChair, 2021}}
Download PDFOpen PDF in browser