4 ms·
Yes, the code in the proof can produce a new prime from a given list (exceptionally slowly); but "constructive" in Lean's context means "does not depend on any
by ykonstant 3y ago
Yes, the code in the proof can produce a new prime from a given list (exceptionally slowly); but "constructive" in Lean's context means "does not depend on any Lean axioms" and I do depend on propositional extensionality which is an axiom.
- gowld 3y agoHow does that definition compare to the usual sense of "constructive"?
- ykonstant 3y agoI don't know, for two reasons: one, I am not sure about the relationship between the foundational type system Lean uses (the Calculus of Inductive Constructions) and usual set theories. Two, there is more than one notion of constructiveness, and I do not care to dig into the semantics of each. Myself, I am not a constructivist in any way. I just like to produce data whenever I can, and I believe that sometimes constructive proofs give additional insights for the objects we study; therein lies my interest in constructive arguments.
- gowld 3y agoI was asking a less sophisticated question. I think the answer is "Lean is constructive if you use the base system without known non-constructive axioms".
- eru 3y ago> Myself, I am not a constructivist in any way. I just like to produce data whenever I can, and I believe that sometimes constructive proofs give additional insights for the objects we study; therein lies my interest in constructive arguments. Constructive proofs also have an interesting relationship with algorithms to construct the object in question. (Funny enough, to proof some algorithms correct, you can use non-constructive proofs.)