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.
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.
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...
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!
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
@@RicardSM 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."
@@RicardSM 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.
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?
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?
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.
@@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 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.
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.
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.
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)
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')
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.
@@maxd.9677 maybe now you are supposed to write "namespace nat" where "open nat" and "close nat" when you want to exit the namespace.
@@Omeomeom I think it is another problem.
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...
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!
Thank you for that, I really struggled with starting with lean : )
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
What is an example of an article that doesn't define the variables they use?
@@RicardSM 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."
@@RicardSM 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.
Thank you for teaching me a really fun new way of validating mathematical proofs
so far the best lean intro I have watched!
Now I'm interested!
I want to work on group theory using this. Where to look for syntax and preliminaries ?
library_search, the magic word...
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?
Thanks for the tutorial
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?
you can't type on the right side, only on the left side
Is there a place that shows all the theorems that Lean currently has?
What's the Lean 4 equivalent of library_search?
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?
what version of lean is this?
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?
The speaker is Scott Morrison
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.
@@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.
@@MrWabouz but the syntax is pretty easy to learn as compared to the actual mathematics in that syntac
@@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.
I'm gonna press like. Oh it's and exactly 100, not gonna ruin the evenness =P
The "use" tactic does not work on Lean Web Editor :(
Is this kevin buzzard with hair
That is exactly what I am thinking about right now 😂
how do you type the reverse Epsilon???
\exists
They send me to learn this tool
It must be worthy it
Cream on aussie maths bloke
Man, your eyes are darkcircled af. Make sure to have enough sleep too.
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.