4 ms·

Does constructive here mean that you can always find a new prime given a set of primes you "think" are all the ones that exist?

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 ago
  How does that definition compare to the usual sense of "constructive"?
  - ykonstant 3y ago
    I 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 ago
      I 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.)
eru 3y ago
I think it's actually fairly hard (or at least non-trivial) to come up with a non-constructive proof of the infinity of primes? For example, Euclid's classic proof (the one that goes 'multiply all the primes you know, add 1') is at least implicitly constructive, because you can factor that new number with a well-known algorithm to get at least one new prime.
- gowld 3y ago
  It's a non-constructive proof. Saying "you could extend the proof to be constructive for a single n" doesn't make it a constructive proof for all n. Infinity is quite a bit bigger than 1.
  - MoonlitKnight 3y ago
    Euclid's proof is constructive in that it describes a procedure which, given a list of primes, computes a prime not on that list. Or equivalently, given a number n it computes a prime > 1.
  - eru 3y ago
    Are you familiar with induction?
empath-nirvana 3y ago
Multiply all known primes together, add 1, factor the resulting number. There will be at least one new prime in the resulting factorization. The "factorization" part can take a _very_ long time, though.
Someone 3y ago
The ’standard’ proof of the infinitude of primes implies that: Given primes p1, p2, …, pn, multiply them, add 1, and factor the result. All its prime factors are new primes. For example, given {5,7,11}, the product is 385. Adding one yields 386. Factoring that learns you that 386 = 2 × 193. Both are primes not in the original list. If you start with {}, the series you get is {} ⇒ 2 = 2 {2} ⇒ 3 = 3 {2,3} ⇒ 7 = 7 {2,3,7} ⇒ 43 = 43 {2,3,7,43} ⇒ 1807 = 13 × 139 {2,3,7,43,13,139} ⇒ 3263443 = 3263443 (https://oeis.org/A126263 https://oeis.org/A126263; i think it doesn’t generate all primes)
- eru 3y ago
  I would be interested in seeing the list of primes not generated by this process. (I wonder whether you need to be able to factor efficiently to get your hands on that list, or whether there's some way around that.)

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 ago
How does that definition compare to the usual sense of "constructive"?
- ykonstant 3y ago
  I 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 ago
    I 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.)

eru 3y ago

I think it's actually fairly hard (or at least non-trivial) to come up with a non-constructive proof of the infinity of primes? For example, Euclid's classic proof (the one that goes 'multiply all the primes you know, add 1') is at least implicitly constructive, because you can factor that new number with a well-known algorithm to get at least one new prime.

gowld 3y ago
It's a non-constructive proof. Saying "you could extend the proof to be constructive for a single n" doesn't make it a constructive proof for all n. Infinity is quite a bit bigger than 1.
- MoonlitKnight 3y ago
  Euclid's proof is constructive in that it describes a procedure which, given a list of primes, computes a prime not on that list. Or equivalently, given a number n it computes a prime > 1.
- eru 3y ago
  Are you familiar with induction?

empath-nirvana 3y ago

Multiply all known primes together, add 1, factor the resulting number. There will be at least one new prime in the resulting factorization. The "factorization" part can take a _very_ long time, though.

Someone 3y ago

The ’standard’ proof of the infinitude of primes implies that: Given primes p1, p2, …, pn, multiply them, add 1, and factor the result. All its prime factors are new primes. For example, given {5,7,11}, the product is 385. Adding one yields 386. Factoring that learns you that 386 = 2 × 193. Both are primes not in the original list. If you start with {}, the series you get is {} ⇒ 2 = 2 {2} ⇒ 3 = 3 {2,3} ⇒ 7 = 7 {2,3,7} ⇒ 43 = 43 {2,3,7,43} ⇒ 1807 = 13 × 139 {2,3,7,43,13,139} ⇒ 3263443 = 3263443 (https://oeis.org/A126263 https://oeis.org/A126263; i think it doesn’t generate all primes)

eru 3y ago
I would be interested in seeing the list of primes not generated by this process. (I wonder whether you need to be able to factor efficiently to get your hands on that list, or whether there's some way around that.)