Infinitude of primes --- a Lean theorem prover demo

[@phlimy]

I tried following the demo and the celebratory message was not accompanied by a party popper emoji. This is unacceptable, how am I supposed to be motivated to write proofs without this ? In all seriousness, this is awesome, thank you.

[@tfae]

I think the reason for that is it's possible to have no goals but still not be done (e.g. because there's an error)

[@minerscale]

Beautiful tutorial, really sympathetic to the beginner who knows nothing. Actually *telling* us that you're leveraging information you already know and otherwise explaining why things are the case. Thank you very much!

[@AndreyRukhin]

For any interested party: as of this writing, 'fact N + 1' no longer evaluates to 'N! + 1'; one my type 'factorial N + 1'. (or 'N! + 1')

[@maxd.9677]

Thanks. I also had a further problem with an error "ambiguous overload, possible interpretations - prime ?? nat.prime ??". This can be fixed by dropping "open nat" and putting by hand the "nat" in front of everything from this namespace, e.g. "nat.prime", "nat.min_fac" etc.

[@Omeomeom]

@@maxd.9677 maybe now you are supposed to write "namespace nat" where "open nat" and "close nat" when you want to exit the namespace.

[@maxd.9677]

@@Omeomeom I think it is another problem.

[@EngineerNick]

This is magic. It's like math but with understandable and consistent syntax. I can't read most wiki articles about math concepts but i feel like I could learn to read this. My main beef is that the articles will often use about 5 alphabetical / greek characters and then neglect to explain what 3 of them mean. To me this feels like a great leap forward for math in general

[@Croqueta-s1f]

What is an example of an article that doesn't define the variables they use?

[@21morpha]

​@@Croqueta-s1f I was thinking about that. What usually happens to me is I don't notice where the variable I'm struggling with was defined in a not well written book section, and I get mad like "where the hell did this phi came from? Come on, he mentions phi without telling me what phi is! Defining phi should be the first thing he did! How could he... Oh, it is the first thing he did. Okay, let's move on."

[@inflivia]

@@Croqueta-s1f The wikipedia page for Taylor's Theorem doesn't define the ! notation. Factorial notation frequently not defined, it's just assumed you know it. I'm sure there are many such examples.

[@imeakdo7]

​@@infliviaright. That's because it's aimed at mathematicians. It's like a technical article in any other field except it's not so obvious

[@inflivia]

@@imeakdo7 did you read the original complaint about articles not defining characters?

[@fhcsghgggfghghhggg4566]

here's the same code but for Lean4: import Mathlib.Tactic.Linarith import Mathlib.Tactic import Mathlib open Nat theorem infinite_primes : ∀ N : ℕ ,∃ p ≥ N , Nat.Prime p := by intro N let M := N.factorial + 1 let p := Nat.minFac M have h0 : Nat.Prime p := by refine minFac_prime ?n1 have : N.factorial > 0 := by exact factorial_pos N linarith use p apply And.intro { by_contra h have h1 : p ∣ Nat.factorial N + 1 := by exact minFac_dvd M have h2 : p ∣ Nat.factorial N := by refine h0.dvd_factorial.mpr ?_ exact Nat.le_of_not_ge h have h3 : p ∣ 1 := (Nat.dvd_add_right h2).mp h1 exact Nat.Prime.not_dvd_one h0 h3 } { exact h0 }

[@nicolasrouquette7817]

library_search, suggest and show_term are powerful tools for developing proofs! I wonder what else is available in the arsenal of a fast & furious lean hacker...

[@livarot1]

Thank you for that, I really struggled with starting with lean : )

[@sudhansubhushanmishra]

Thank you for teaching me a really fun new way of validating mathematical proofs

[@benji104]

so far the best lean intro I have watched!

[@Spiritusp]

library_search, the magic word...

[@cryptoholic01]

Now I'm interested!

[@saigopal4361]

I want to work on group theory using this. Where to look for syntax and preliminaries ?

[@tolkienfan1972]

Very cool.

[@edeneden97]

Thanks for the tutorial

[@evgenysmirnov4506]

So why the assistant could not succeed at library_search, but could suggest a lemma and, in context of this lemma, succeeded at library_search? Is the lemma unsafe in some sense or is this second-order search deemed too hard in general case?

[@thedude4795]

I'm gonna press like. Oh it's and exactly 100, not gonna ruin the evenness =P

[@MrWabouz]

Cool presentation. I just discovered Lean and I couldn't see how it was an interesting tool before this video! May I ask for the speaker's name?

[@leanprovercommunity5485]

The speaker is Scott Morrison

[@fyradur]

If you didn't find it interesting before, you probably still don't understand why it's actually interesting. It's interesting because most of mathematics has never been formally verified, we just have 100% faith in people with fancy titles from universities. And let's say you are a random broke person with no academic degree, but you have an interest in math on your free time, and you found the proof of the Riemann Hypothesis, but it took 1000 pages. Will anybody read that? No. But with this software that person could write it in this software and the rest of the world could verify it by just checking if the code compiles correctly.

[@MrWabouz]

@@fyradur I didn't find it interesting because I can read and write mathematical proofs without that ;) I still think it's not worth for everyone to have to struggle with a programming language syntax to express elegant and novel ideas and mathematical concepts.

[@suryanshshrivastava4681]

@@MrWabouz but the syntax is pretty easy to learn as compared to the actual mathematics in that syntac

[@MrWabouz]

@@suryanshshrivastava4681 You'll have to convince me that this programming language could allow anyone create new mathematical methods, concepts and tools before I can agree with you ;) I have always enjoyed the freedom offered by a whiteboard, not sure I'm ready to forfeit that.

[@xxnotmuchxx]

Is there a place that shows all the theorems that Lean currently has?

[@xxnotmuchxx]

I am not a mathematician but I was wondering if u can type the right side (tactic state section) and get the software to convert it into code or is the right side general information? Also, is it possible to learn math using Lean?

[@unarei]

you can't type on the right side, only on the left side

[@JosiahWarren]

Is this kevin buzzard with hair

[@مجتبىعلي-د1خ]

That is exactly what I am thinking about right now 😂

[@ktgideon3053]

They send me to learn this tool It must be worthy it

[@whozz]

The "use" tactic does not work on Lean Web Editor :(

[@nidhoggroom]

Is the language like "fact" and "min_fac" a universal language? i.e could this be built in Wolfram Mathematica CDF as well, by doing a copy paste?

[@bobvance9519]

What's the Lean 4 equivalent of library_search?

[@fhcsghgggfghghhggg4566]

it's 'exact?'. and the equivalent of suggest is 'apply?'. i added a comment under the video with a full Lean4 code (at least i tried to. it seems as if youtube is shadow banning me again)

[@bobvance9519]

@@fhcsghgggfghghhggg4566 Thanks

[@bobvance9519]

@@fhcsghgggfghghhggg4566 Thanks

[@bobvance9519]

@@fhcsghgggfghghhggg4566 Thanks

[@bobvance9519]

@@fhcsghgggfghghhggg4566 Thanks

[@amosdominion9502]

what version of lean is this?

[@fhcsghgggfghghhggg4566]

the video probably uses Lean3

[@felixlucien7375]

Cream on aussie maths bloke

[@danielsmith5626]

how do you type the reverse Epsilon???

[@krisburashi2344]

\exists

[@reactionaction4845]

Man, your eyes are darkcircled af. Make sure to have enough sleep too.

[@JosiahWarren]

I am pretty sure you have used in the proof of contradiction the hypothesis. Min_fac_prime. For the love of god as a senior developer you have to improve your naming coventions and the context display for what the lemmas on search do, this would be unacceptable way of writing code in any other domain. You cannot just try to guess what the lemma do. Its so opaque. We have alot of work to do. Mathematicians should learn programming.

[@98danielray]

it is very clear what the lemma does and the naming conventiong. "prime not divide one".