Factor De Bruijn

El factor de De Bruijn es una medida de la dificultad de escribir una demostración matemática formal en comparación con una informal . Fue creado por el pionero holandés de las demostraciones computacionales, Nicolaas Govert de Bruijn .

De Bruijn lo calculó como el tamaño de la prueba formal sobre el tamaño de la prueba informal . ^{[ 1 ]}

Freek Wiedijk perfeccionó la definición para utilizar el tamaño comprimido de la prueba formal sobre el tamaño comprimido de la prueba informal. A esto lo llamó el "factor intrínseco de De Bruijn". La compresión elimina el efecto que podría tener la longitud de los identificadores en las pruebas. ^{[ 2 ]}