5 ms·
Touting my own horn a bit, I have a constructive* proof [0] of the infinitude of prime numbers from first principles: there is no dependence on mathlib so I bui
by ykonstant 3y ago
Touting my own horn a bit, I have a constructive* proof [0] of the infinitude of prime numbers from first principles: there is no dependence on mathlib so I build all the concepts from scratch. I have been thinking about turning it into a literate code document.
*The only axiom I cannot avoid is propositional extensionality (which is kind of unavoidable in any non-toy proof in Lean).
[0] https://github.com/ykonstant1/InfinitePrimes https://github.com/ykonstant1/InfinitePrimes
- frabert 3y agoDoes 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 agoYes, 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.)
- eru 3y agoI 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 agoIt'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 agoEuclid'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 agoAre you familiar with induction?
- empath-nirvana 3y agoMultiply 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 agoThe ’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 agoI 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.)
- tux3 3y agoI love that Lean completely destroys any suspicion of crackpottery. There's a common trope of internet comments where you see people say they went off and did their own thing from first principles, pointedly avoiding existing work and preferring to follow their own ideas. And then you look at the thing and it's nigh invariably the disconnected ramblings of a person convinced of their own misunderstood genius. But if the computer vouches for you, hard to avoid taking it seriously, that's the highest standard of rigor we have :) (Nice proof by the way!)
- ykonstant 3y agoI am not important enough to be receiving crackpot proofs, but if I ever do, I will enthusiastically suggest they formalize their work in Lean. Hmm, I wonder whether that would lead to crackpots making a fuss at the Zulip chat.
- hucker 3y ago> I have been thinking about turning it into a literate code document. Please do! This looks like the perfect size and complexity to learn the basics, I'd love a structured walk-through of the code.