4 ms·
A slightly longer Lean 4 proof tour
- esafak 3y agoIf I understand correctly, this is the dependency graph of all the conjectures involved in the proof: https://terrytao.files.wordpress.com/2023/11/image.png https://terrytao.files.wordpress.com/2023/11/image.png It really makes the complexity of a proof more tangible, even if it does not capture the complexity of proving each step.
- gexaha 3y agoNot quite, this blogpost is about a different problem
- SkyMarshal 3y agoPrior discussion of Terry’s first post on the subject: https://news.ycombinator.com/item?id=38528582 https://news.ycombinator.com/item?id=38528582
- woolion 3y agoSee also https://news.ycombinator.com/item?id=38035672 https://news.ycombinator.com/item?id=38035672, a discussion a month prior about how he used AI copilot to help him get into Lean4.
- ykonstant 3y agoTouting 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.)
- hrldcpr 3y agoI like the phrase "in a civilized fashion", I wonder what he means by that—no chatbots?
- gowld 3y agoI think it means human-friendly: not 50pages of arcane symbols; referring to welle known theorems instead of inclining the proofs.
- gowld 3y agoI'm confused. The tweet doesn't say that a_n is monotone nom-increasing, but the theorem isn't true for non monotonic a_n. D_0 = 10, D_1 = 10, D_2 = 1 a_0 = 0, a_1 = 9 ≤ 10/(1+1) is false https://twitter.com/damekdavis/status/1730983634570510819/photo/1 https://twitter.com/damekdavis/status/1730983634570510819/ph... Tao's proof assumes a_n is monotonic non-increasing. Did the OP tweet just make a mistake that Tao ignored?
- 3PS 3y agoThe original tweeter made a follow up tweet clarifying that a_n should indeed be non-increasing. https://twitter.com/damekdavis/status/1730984627030905209?t=YOkzkon0swJuDbwFdilvhQ&s=19 https://twitter.com/damekdavis/status/1730984627030905209?t=...