De Bruijn criterion

The de Bruijn criterion is the requirement for formal proofs to be expressed in a small subset of the language available to a proof assistant, allowing them to be checked by small independently developed computer programs that can check the validity of statements in that small language. Such programs are known as proof checkers or "kernels", and are intended to be small enough to be checked by human beings, allowing even very large machine-generated proofs to be grounded in terms of human-created axiomatic systems.

The criterion was named by Henk Barendregt after Nicolaas de Bruijn, who founded the field of automated theorem proving.

The Coq and Lean proof assistants can both emit proofs which meet the de Bruijn criterion.

References

1 2 "What's a kernel? - Type Checking in Lean 4". ammkrn.github.io. Retrieved 2026-11-11.
1 2 Chlipala, Adam (2013). Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. Cambridge, MA: The MIT Press. ISBN 978-0-262-02665-9.
↑ Geuvers, Herman; Nederpelt, Rob (2013-11-15). "N.G. de Bruijn's contribution to the formalization of mathematics". Indagationes Mathematicae. In memory of N.G. (Dick) de Bruijn (1918–2012). 24 (4): 1034–1049. doi:10.1016/j.indag.2013.09.003. ISSN 0019-3577.
↑ Barendregt, Henk; Wiedijk, Freek (2005-10-15). "The challenge of computer mathematics". Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 363 (1835): 2351–2375. doi:10.1098/rsta.2005.1650. ISSN 1364-503X.

This mathematics-related article is a stub. You can help Wikipedia by adding missing information.

This computer science article is a stub. You can help Wikipedia by adding missing information.

[leanbook-1] 1 2 "What's a kernel? - Type Checking in Lean 4". ammkrn.github.io. Retrieved 2026-11-11.

[coqbook-2] 1 2 Chlipala, Adam (2013). Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. Cambridge, MA: The MIT Press. ISBN 978-0-262-02665-9.

[3] Geuvers, Herman; Nederpelt, Rob (2013-11-15). "N.G. de Bruijn's contribution to the formalization of mathematics". Indagationes Mathematicae. In memory of N.G. (Dick) de Bruijn (1918–2012). 24 (4): 1034–1049. doi:10.1016/j.indag.2013.09.003. ISSN 0019-3577.

[4] Barendregt, Henk; Wiedijk, Freek (2005-10-15). "The challenge of computer mathematics". Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 363 (1835): 2351–2375. doi:10.1098/rsta.2005.1650. ISSN 1364-503X.