De_Bruijn_factor

De Bruijn factor

De Bruijn factor

Add article description

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[clarify].[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. [1]
    Wiedijk, Freek. "De Bruijn Factor". Radboud University. Retrieved 11 January 2022.
  2. [2]
    Wiedikj, Freek. "The De Bruijn Factor" (PDF). Radboud University. Retrieved 11 January 2022.
Share this article:

This article uses material from the Wikipedia article De_Bruijn_factor, and is written by contributors. Text is available under a CC BY-SA 4.0 International License; additional terms may apply. Images, videos and audio are available under their respective licenses.