De Bruijn Factor

The de Bruijn Factor is a measure of how much harder it is to write a formal mathematical proof instead of an informal one. It was created by the Dutch computer-proof pioneer Nicolaas Govert de Bruijn.

De Bruijn computed it as the size of the formal proof over the size of the informal proof.[1]

Freek Wiedijk refined the definition to use the compressed size of the formal proof over the compressed size of the informal proof. He called this the "intrinsic de Bruijin Factor". The compression removes the effect that the length of identifiers in the proofs might have.[2]

References
  1. Wiedijk, Freek. "De Bruijn Factor". Radboud University. Retrieved 11 January 2022.
  2. Wiedikj, Freek. "The De Bruijn Factor" (PDF). Radboud University. Retrieved 11 January 2022.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.