The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

[For those not following closely: Law of Excluded Middle can be derived from Axiom of Choice + a couple of extensionality axioms]

Sure, Axiom of Choice useful to prove that every ideal is contained within a maximal ideal (the argument is known as Zorn’s lemma, math.AC), and Tychonoff's compactness theorem (math.GN) is essentially equivalent to the axiom. However, in Algebraic Geometry, one works with Noetherian rings, for which the weaker Axiom of Dependent Choice is sufficient.

What’s the harm in having Axiom of Choice turned on by default? Two things. First, it has consequences that are simply untrue, for instance, in Lie categories. Second, picking axioms that are stronger-than-necessary to do a mathematical proof is unacceptable.

--

Since I highlighted Differential Geometry in my previous note, let us look at an example that seems particularly tricky to formalize in our current proof-assistant world: the elliptization conjecture (commonly known as the Poincaré conjecture), which was solved by Perelman in 2003, over a span of three papers (https://arxiv.org/search/?query=grisha+perelman&searchtype=author&abstracts=show&order=-announced_date_first&size=50). Incidentally, Perelman was awarded a Fields Medal for his work.

--

Coq’s math-comp is an axiom-free formalization.

R.