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
Nicolaas Govert (Dick) de Bruijn (; 9 July 1918 – 17 February 2012) was a Dutch mathematician, noted for his many contributions in the fields of analysis, number theory, combinatorics and logic. .
De Bruijn computed it as the size of the formal proof over the size of the informal proof.
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.
References
{{reflist
Mathematical logic