デ・ブルイン因子

デ・ブルイン係数は、形式的な数学的証明を書くことが、非形式的な証明を書くよりもどれだけ難しいかを示す指標である。これは、オランダのコンピュータ証明の先駆者であるニコラース・ゴヴェルト・デ・ブルインによって考案された。

デ・ブルインはそれを形式的証明のサイズを非形式的証明のサイズで割ったものとして計算した。^{[ 1 ]}

フリーク・ヴィーダイクは、形式的証明の圧縮サイズを非形式的証明の圧縮サイズよりも優先して使用するように定義を改良した。彼はこれを「内在的デ・ブルイン因子」と呼んだ。圧縮により、証明における識別子の長さが及ぼす影響が取り除かれる。^{[ 2 ]}