A slightly longer Lean 4 proof tour | Hacker News Reader

A slightly longer Lean 4 proof tour

terrytao.wordpress.com

78 pointsiso8859-127 comments

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

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?

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.

How does that definition compare to the usual sense of "constructive"?

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.

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".

> 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.)

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.

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.

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.

Are you familiar with induction?

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.

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; i think it doesn’t generate all primes)

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.)

I 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!)

I 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.

I think anything that increases the amount of reasoning exercised by humans is a noble endeavor, regardless of the underlying cause.

given the crackpot proofs received by coq-club, i imagine it would indeed

> 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.

If 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

It really makes the complexity of a proof more tangible, even if it does not capture the complexity of proving each step.

Not quite, this blogpost is about a different problem

I'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/ph...

Tao's proof assumes a_n is monotonic non-increasing.

Did the OP tweet just make a mistake that Tao ignored?

The original tweeter made a follow up tweet clarifying that a_n should indeed be non-increasing.

https://twitter.com/damekdavis/status/1730984627030905209?t=...

Prior discussion of Terry’s first post on the subject: https://news.ycombinator.com/item?id=38528582

See also https://news.ycombinator.com/item?id=38035672, a discussion a month prior about how he used AI copilot to help him get into Lean4.

I like the phrase "in a civilized fashion", I wonder what he means by that—no chatbots?

I think it means human-friendly: not 50pages of arcane symbols; referring to welle known theorems instead of inclining the proofs.

Reply on news.ycombinator.com