Constructive Proof

A constructive proof in mathematics establishes that some mathematical object exists by actually building it, or by giving an explicit method for building it, in contrast to a non-constructive proof, which can establish existence without ever producing an example. The term also describes proofs that are valid within constructive mathematics, an approach to mathematics that rejects methods relying on objects that are never explicitly constructed, including the unrestricted use of the law of the excluded middle, the axiom of infinity, and the axiom of choice, and that gives some ordinary logical words, such as or, a different meaning from their classical one. Constructive proofs are connected to certified computer algorithms through results such as the Brouwer-Heyting-Kolmogorov interpretation, the Curry-Howard correspondence, Per Martin-Loef's intuitionistic type theory, and the calculus of constructions developed by Thierry Coquand and Gerard Huet. This description is adapted from Wikipedia contributors under CC BY-SA 4.0; changes were made. https://creativecommons.org/licenses/by-sa/4.0/