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.

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.