{{Short description|Mathematical concept}} 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 {{clarify span|size of the informal proof|reason=This would require a formal language for informal proofs, which seems a self-contradictory requirement. Moreover, informal proofs come with different levels of detail, and hence length. For example, the proof that some particular function is continuous is usually much more explicit in a beginner's course (to provide additional practice in proving functions continuous) than in an advanced course (where it is often considered a trivial detail left to the student).|date=February 2024}}.<ref>{{cite web |last1=Wiedijk |first1=Freek |title=De Bruijn Factor |url=https://www.cs.ru.nl/~freek/factor/ |website=Radboud University |access-date=11 January 2022}}</ref>
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 Bruijn Factor". The compression removes the effect that the length of identifiers in the proofs might have.<ref>{{cite web |last1=Wiedijk |first1=Freek |title=The De Bruijn Factor |url=https://www.cs.ru.nl/~freek/factor/factor.pdf |website=Radboud University |access-date=11 January 2022}}</ref>
== References == {{reflist}}
Category:Mathematical logic