We have money. Come over. -United States of We Can Fund This and Change the World with Your Logical Dreams of a Better Future of Mathematics-
@halian.vilela
6 күн бұрын
Done!
@netizenkane2230
3 жыл бұрын
Ha! I love this guy. His statement about "proper mathematicians" is gold!
@madvorakCZ
3 жыл бұрын
This is the best lecture and the best KZitem video ever! I've never watched anything more enjoyable!
@luisfernandoalves2748
2 ай бұрын
I remember listening to this when it came out four years ago and now I came back here after I learned that Lean is being used by DeepMind to expand and train their A.I models to learn and prove new theorems. Turns out the speaker was spot on. This is the future.
@volotat
5 жыл бұрын
Amazing lecture. I would love to hear more from this guy.
@apolloapostolos5127
5 жыл бұрын
Anak Wannaphaschaiyong . ?
@PrzemekChojeckiAI
4 жыл бұрын
Great lecture by Kevin Buzzard, especially knowing him from number theory circles.
@BattousaiHBr
3 жыл бұрын
somehow his name is nowhere in the video description nor title.
@NavdeepVarshney-ep4ck
5 ай бұрын
Are u doing research in number theory by using circle method
@alexscofield1198
Ай бұрын
I actually followed a course in Orsay, by the very teacher mentioned in the lecture. Absolutely top notch. I instantly fell in love with Lean
@rickharold7884
5 жыл бұрын
Fascinating. Amazing how profs are accepted and not fully validated. Software looks super cool and is a key to helping
@MrBrew4321
3 жыл бұрын
Yea it's crazy how rickshaw piece meal math is. Crazy how cool mathematicians seem to be about that status quo. When computers take over for us they may throw out a lot of stuff that didn't actually logically flow
@LV-426...
3 жыл бұрын
The most amazing thing is how a professor who talks about the formalization of math consistently uses the word "invented".
@traveldiaryinc
5 жыл бұрын
Please include the presenter's name in the description.
@weimondo
5 жыл бұрын
Kevin Buzzard
@danielurbinatoro9496
4 жыл бұрын
I think the presenter is: leodemoura.github.io/
@FingersKungfu
3 жыл бұрын
So Prof Kevin Buzzard's goal is to formalize all the elementary textbooks of mathematics, the whole body of math, and create the modern "Elements." This can be the turning point of mathematics in this century.
@jacobchateau6191
3 жыл бұрын
69420 views, nice. Also, automated theorem proving is absolutely the future! How much do you want to bet that the first AGI will be a higher monad implemented in a formal proof language?
@thetedmang
5 жыл бұрын
Computational mathematician master race checking in. Enjoy your single-subject expertise in your silos, pedagogues. Just kidding. Good talk. The world of mathematics will be blown wide open once we fully harness the power of the PC.
@skurtz97
Жыл бұрын
It's amazing just how similar mathematics is to software development once either gets to a large enough scale. When he's talking about "the proof is correct because the elders said so", I couldn't help but think of a parallel with all the vulnerabilities and bugs software engineers import on a daily basis from "libraries the elders have accepted", and we are okay with it because we know it works and "small errors don't matter and we can work around them". No mathematician fully understands Wiles' proof just as no programmer fully understands the Linux kernel, but we are all obligated to accept both.
@DSCH4
5 жыл бұрын
Alternative title: "Number Theorist Finds Cheap and Highly Productive Manner In Which to Have a Mid-Life Crisis" XD 16:58
@sergiogomez1008
5 жыл бұрын
I'm curious if he got his new computer, it seemed important... 32:10
@kellymoses8566
2 ай бұрын
Imagine having every proven theorem encoded in Lean and you could verify all of them at the press of a button.
@BhrantoPathik
4 ай бұрын
What a talk man!!! ❤
@g1m0kolis
5 жыл бұрын
I hope those pants are an indication of future mathematics!
@tacopacopotato6619
5 жыл бұрын
This stuff looks really cool. Might have to check out this scene a little
@ferhattas4794
5 ай бұрын
This will become Modern Mathematics.
@rickandelon9374
14 күн бұрын
At 9:10 He said computers will beat humans at math in 10 years. Well the most it will take is 7-8 years when o3/GPT7 will be released. They will have way more advanced reasoning than humans, have infiinite context and find connections in various literatures.
@hypergraphic
5 жыл бұрын
Wow, I never realized academics is so political and, well , human and subject to all of the foibles of ego.
@RafaelSCalsaverini
5 жыл бұрын
Oh yeah it is. Even more so than many other fields.
@alan2here
5 жыл бұрын
Good sort of lecturer to have around as a student though. :)
@jpratt8676
4 жыл бұрын
That's the one good thing about computer science. People are using it to make money, so of a system is broken we often notice.
@jpratt8676
4 жыл бұрын
The bad part is that once we notice we don't necessarily fix it
@andrybak
4 жыл бұрын
Science trends are more trendy than fashion trends. Same is also often said about computer programming. Recently, especially in the context of JavaScript frameworks.
@bbsara0146
2 ай бұрын
my coq is extremely hard
@MrM12LRV
5 жыл бұрын
Category theory and type theory are nice. Why regard them as something other than proper?
@jonhillery7736
5 жыл бұрын
Because nobody outside of those areas really care about them currently
@MrM12LRV
5 жыл бұрын
@@jonhillery7736 Ah, but they provide nice isomorphisms, so if something is discovered in category theory, then we will have an analogous concept discovered elsewhere. : ) which is pretty cool and worthwhile in my opinion. People are attracted to a particular topic, naturally, and they will indirectly solve a problem in another topic!
@fbkintanar
5 жыл бұрын
I think he means that "proper" mathematicians, the vast majority, are not working in foundations and don't bother to try to follow current work in foundations like category theory. Many research mathematicians will use a bit of category theory as a tool or a language for something they also think of in another way, but they won't see category theory as a source of new ideas that they care about. Category theory works at the level of "objects" and what connects them (i.e., groups and homomorphisms, up to isomorphism and never "on the nose," it won't care about constructing a particular homomorphism). By design categories are blind to the elements of objects and things like multiplication tables (Cayley tables) that define particular groups. Category theory can't work at the level where one element equals another, it only works at the level where two objects are isomorphic (or categorically equivalent, or left adjoint or something...) and so will only take a "proper" mathematician so far before they have to move back to the level of the elements of the structures they are interested in. Many mathematicians know something about universal properties and think they are a good thing, but it doesn't make them want to read papers on category theory, or approve applications to their department from category theorists or mathematical logic researchers. It's like most mathematicians will use set operations and axiom systems, but are completely uninterested in recent work in set theory or logic. They think, those fields are like Euclidean plane geometry, it's nice and useful but completely understood. There is nothing new to discover for a researcher.
@power9k470
2 жыл бұрын
Too general to create something substantial.
@columbus8myhw
5 жыл бұрын
That's a whole lot of railing against the old guard without ever using the words "old guard". Though the word "elder" is used which I suppose means the same thing
@columbus8myhw
5 жыл бұрын
There's a concrete plan and call to action
@0xlemi
3 жыл бұрын
Great video!
@vasiovasio
5 жыл бұрын
The future of mathematics is digital!
@paulgoogol2652
5 жыл бұрын
let's get digital, digital. I want to get digital.
@vasiovasio
5 жыл бұрын
@@paulgoogol2652 Yes! play the video :) kzitem.info/news/bejne/kZ582airrHaLgaAm56s
@dialecticalmonist3405
3 жыл бұрын
Mathematics is a language of intuition. Computer science is an interface between languages. Language itself is an intuition of correspondence. All these systems will eventually prove, is that intuition is more fundamental than logic.
@valentindiaz4567
3 жыл бұрын
Where can I look for more information about Lean?
@ezrakhayyam5609
Жыл бұрын
@1:02:50 someone knows what is this system he is talking about "errands" ?
@Pr3da70rl0rd
5 жыл бұрын
I am just fascinated by the degree to which mathematicians are not benefiting from tools that essentially emerged from mathematics, yet thinking about the level of technology utilisation by educational institutions, for educational purposes, I kind of get back on Earth remembering the 'sad' reality where we are wasting our collective efforts on trivial endeavours ..
@volution1160
Жыл бұрын
Tradition in teaching and Lean (including CIC) is pretty hard to understand
@ton1
3 жыл бұрын
5:50 You have to ask the Elders of the Internet
@alan2here
5 жыл бұрын
Automatically enumerate _All_The_Proofs_, in magnitude order :) In x^x time complexity :( Except it's also the Xth hyper-operation :( And all but a vanishingly small subset are provably unprovable :( I hope it's not that hard. 🤷🏻♂️
@questioneverythingalways820
3 жыл бұрын
Literally outlines the issues with current academic systems at 13:00 ish
@corochena
3 жыл бұрын
It seems to me they are teaching computers how to do math, just as a few decades ago they were able to teach computers to play chess... I think they will succeed
@alexandersanchez9138
5 жыл бұрын
Wow. This is an inspiring talk.
@itssoveryeasy
5 жыл бұрын
A century after Kurt Gödel, a number theorist says terms like "intellectual domination, and others have nothing to offer". Really! I feel sad and sorry for him, his students and his audience.
@paulgoogol2652
5 жыл бұрын
lol what a nerd
@bassamkarzeddin6419
5 жыл бұрын
@@paulgoogol2652 You have to be a little patient to understand the issue, by the way (Do you see my comment 2 hours ago, I think it is still on the top of comments as I do see it from my computer? Thanks
@FistroMan
5 жыл бұрын
There is a probality about Gödel have proved, in an unsufficient way, his theorem. So be carefull about 'the way' you say what you are thinking: probably you will need to eat that words in a near future. Remember to be nice always, it's a better way to express yourself.
@paulgoogol2652
5 жыл бұрын
@@bassamkarzeddin6419 I see. Good comment.
@itssoveryeasy
5 жыл бұрын
@@FistroMan hey! Probability is a substory of number theory, so that's also discardable. I get there should be civility in public discourse. But, that shouldn't imply we start respecting ape shitery. I should be able to call something stupid, "stupid", otherwise what's the point of freedom of expression, if it's just for flowery words, which mean nothing.
@shannonchuprevich3021
5 жыл бұрын
I find this worthy to invest in. There is potential for this type of application in ALL fields. As a proper ally\friend\family we should look out for him. It's a much wiser and safer investment compared to just smashing particles together.
@shannonchuprevich3021
5 жыл бұрын
Thank you for allowing me to be a part of the conversation.
@Subliminal8853
Ай бұрын
1:11:30
@jesseburstrom5920
5 жыл бұрын
Ahh open source LEAN got it!
@avimoyal149
5 жыл бұрын
❤
@jiaming5269
4 жыл бұрын
wow.
@dumbass6852
5 жыл бұрын
Hi
@jesseburstrom5920
5 жыл бұрын
Great!!!
@tomekpaluch8164
4 жыл бұрын
The irony is that it is the first search result for "e theorem prover". If exact name of your software isn't enough to find it, you're definitely not hot stuff at the moment. (Note, that you just have to believe me on that - I did the same in Tor, and it was second result. YT like every other big player just likes your personal data too much).
@BennettAustin7
5 жыл бұрын
Why didn’t he just prove the deriv of sin is cos by taking h->0 of sin(x+h)
@hansmeier3065
5 жыл бұрын
this also comes down to a circular argument (as far as I know), because some trig identity used in that proof can not be proven without the deriv of sine
@ginganinga1010
5 жыл бұрын
21:17 "so i think that's kinda weird" lol
@INLF
5 жыл бұрын
There are no numbers in number theory, that's what number theory has become.
@sadface7457
5 жыл бұрын
If numbers themselves divulged structure and pattern of numbers then the field would be barren.
@Trotskisty
5 жыл бұрын
Guys... numbers are an intellectual invention: created to map order and metric onto the Real-World fabric of The Universe. Geometry is PRIMARY. Numbers are Ideal, created out of whole cloth, and PROVISIONAL and SECONDARY. People who put numbers ahead of the geometry of Reality are simply Platonic Idealists, at root -- and might as well be discussing how many angels can dance on the head of a pin.
@dramawind
5 жыл бұрын
it's a common theme in math to jump from simple things to more complex, and use the more complex framework to prove stuff about the simple things
@INLF
5 жыл бұрын
Guys it's a quote from the talk...
@drdca8263
5 жыл бұрын
Trotskisty You are confused. That which follows from a collection of premises follows from those premises. Topics in math do not follow a single linear progression. Many topics can be introduced in a variety of orders, and often either of two topics can be used to introduce or define the other topic. There is no problem in doing this. Either can be done first. The end results are the same. There are many equivalent ways to define the same structures.
@Damodharanjay
5 жыл бұрын
why not z3 ?
@cgibbard
5 жыл бұрын
Z3 is an SMT solver. It tries to decide in a completely automatic way whether there's an assignment of values to variables in a formula to make some equations true. It doesn't really deal with arbitrary quantifiers - there are some tricks it can do to attempt to answer questions in the presence of simple quantifiers, but things break down pretty quickly there. You also can't generally even ask Z3 questions about the existence of simple functions, let alone about the kinds of dependently-typed functions and data which come up in mathematics generally. The thing that Z3 has going for it, is that it's pretty much automatic. You put your question in, and it either gives you a solution or tells you there are none. It's not going to let you explain to *it* why anything is true though.
@digama0
5 жыл бұрын
@@cgibbard It's also not going to explain to you why it thinks anything is true. Z3 is built on a mishmash of heuristics and has no logical foundation underlying it, no "small trusted kernel" as in most ITPs. This is a major reason Leo started Lean in the first place, it's not configurable or rigorous enough.
@cgibbard
5 жыл бұрын
It can't even give you the assignment of values to the variables?
@digama0
5 жыл бұрын
@@cgibbard For pure SAT problems, or existential problems, I think you can get the assignments, but theorem provers are usually interested in proofs of unsatisfiability and I don't think Z3 gives these. There is a pseudo-proof format called TSTP that a lot of SMT solvers support (I forget if Z3 supports it but I think it does), but it's more like a standard format than a standard semantics (it's like XML compared to HTML) so SMT provers can put whatever they like in there.
@csmole1231
5 жыл бұрын
this recommendation of video is waaaaaaaaaaay out of my league😂I'm scared😂
@davidwilkie9551
5 жыл бұрын
If we were mining for the Origin of Mathematical meaning, then the "distillation" of probabilities in potential possibilities represented by the bio-logical sequences of chemical compounds in evolving resonances that follow "sum-of-all-histories" calculus operation of the Temporal Superposition-point Singularity .. "legal precedents" set by actual observable evidence of continuous probability, ..are the only proof of concept proving available?
@money8330
5 жыл бұрын
Can Mathematics cure Parkinson's disease which is a exponentially growing threat........🤔🤔🤔🤔
@mrnarason
5 жыл бұрын
Kevin Buzzard is of course really smart but some of the stuff he said is just in such bad taste. Stuff like, being surprise ungrads can somehow contribute to cutting edge research. That phDs should be dominating over undergrads. Like what the heck. This type of condescension from math professors is why so few people take up a math major in the first place. It like saying a 250 lb body builder and totally destroy a skinny 14 year old he's training in a fight. Like yeah, but there should be some sense of equal grounds and sympathy/understanding, vs looking down or patronizing attitude, which is pretty digusting tbh.
@cgibbard
5 жыл бұрын
I don't think he's making a moral judgement that things really ought to be one way or another, just pointing out that in this case the skinny 14 year old is kicking the heavyweight's ass and the teaching is going in an unexpected direction.
@tobykelsey4459
5 жыл бұрын
@@cgibbard Kevin could have phrased it better but he's implying that in existing fields of mathematics there is a large pyramid of existing knowledge undergraduates have to climb before they can eventually contribute something new at postdoc level, while with the Lean prover they can contribute immediately and become the experts while still undergraduates. He's saying that youth is not a barrier to expertise, so it is in fact an anti-condescending message.
@cgibbard
5 жыл бұрын
@Toby Kelsey Yes, I agree.
@Downloader77
5 жыл бұрын
I genuinely think he means well, and has high expectations of both undergraduates and Phds, you're right his language is a tad off line. From what I know about him he is a gently spoken kind person.
@jamma246
5 жыл бұрын
_"Stuff like, being surprise ungrads can somehow contribute to cutting edge research. That phDs should be dominating over undergrads. Like what the heck. This type of condescension from math professors is why so few people take up a math major in the first place."_ He was being a bit tongue in cheek, but there is a very valid point here. It is _extremely_ rare that undergrads are able to contribute to cutting edge research in pure mathematics. It almost never happens (I know of some cases, but very few - if you'd like to prove otherwise, please give examples). That's not being rude to undergrad students, it's just the reality that it takes an incredible amount of patience, practice, time and experience to learn enough to even begin to get a feel for the state of the art in some research area, and then you still need to come up with interesting questions, and then be able to prove these things. This is totally unreasonable to expect of any undergrad. There will be the occasional wunderkind, but it's very rare. It's not the same as saying that undergrads should be put off, it's just being realistic. Actually, if anything, I think this would be very uplifting for undergrads to hear. If you're struggling: don't worry, it's normal, and you totally can't be expected to come up with new stuff at that level (which isn't the same as saying you shouldn't try! That's a very good way to learn). You don't have to be unusually gifted to contribute to new, interesting pure maths research - it helps if you are - but if you're not (and often even if you are) it is necessary that you will need experience and time to get there. And the "should be dominating over the undergrads"... he didn't say that they should be doing this, or trying to intimidate them. Again, it's just the reality of how difficult it is to understand cutting edge mathematics these days.
@hajdukbesmrtnik802
5 жыл бұрын
CPU... 😉
@OEFarredondo
5 жыл бұрын
A pencil that self sharpens? Eraser that leaves 1/2 the marks? Paper that don’t rip? Idk but it will be pencil and paper till Jesus comes back
@Slimm2240
5 жыл бұрын
If your watching this and understand this, can we be friends?
@FistroMan
5 жыл бұрын
I understand the quarter of it... we can say we know each other.
@paulgoogol2652
5 жыл бұрын
this is no dating site.
@MrAlRats
5 жыл бұрын
*you're
@lchpdmq
5 жыл бұрын
This guy really likes himself😅
@TheKhakPakflyest
5 жыл бұрын
im here trying to be an academic and mature, but this guys just writing the coq jokes himself.
@NothingMaster
5 жыл бұрын
This should have been advertised as An Introduction to The Lean Theorem Prover, NOT The Future of Mathematics. Yes, we are currently facing a crisis at the foundations of mathematics, and tools like the Lean Theorem Prover would go a long way in formalizing category theory, type theory, abstract algebra etc. That said, let’s hope that there is far more in the future of mathematics than just tools like the Lean Theorem Prover.
@bassamkarzeddin6419
5 жыл бұрын
You are right about the crises, and it doesn't require anything behind too elementary math to fully comprehend, See my previous (one-page comment please)
@elliott8175
3 жыл бұрын
It's also a revolution in teaching/learning analysis. The digitalisation and the formalism will also mean being able to review the full "stack" of the math hierarchy down to the axioms. Finally, submission of math papers will likely *_require_* a Lean code submission (or an equivalent language); and will mean that papers take hours to be accepted instead of years. It may also be possible that machine learning could integrate well with languages like Lean to generate certain types of proofs. If so, mathematicians might spend much of their time trying to understand the underlying ideas in computer-generated proofs. Sounds like a revolution to me...
@baseradius3907
5 жыл бұрын
Dude, get on with your talk.. 9 minutes in and you're just rambling about!
@dominicdannies7482
5 жыл бұрын
Mathematicians use clickbait now ... wow
@shivakumarcd
5 жыл бұрын
Real life Sheldon Cooper
@michaelcharlesthearchangel
5 жыл бұрын
Metamathematics (polymathematic; type 0-1 encryption) and Matheautomatics (super AI) are the future of Quantum numbering.
@MMABeijing
5 жыл бұрын
hi brazilian/portuguese guy: get rid of your horrible accent please
@CGoldthorpe
5 жыл бұрын
The guy introducing him has a horrible accent making it VERY difficult to understand him!
@jamma246
5 жыл бұрын
It wasn't for me, I thought it was a nice introduction. Don't be so mean, not everyone is a native English speaker. You probably aren't, given that you couldn't understand him.
@omegabeth3987
5 жыл бұрын
I second staying away from foreign improper coqs so called mathematicians and jus do you and lean with it, age is jus a number drive your Volvo to that undergraduate underground society and be safe. Is this really about “soft ware” sounds sexual to be honest the whole conversation I was keeled over and crying laughing. Anyone else? Coded mssgs sent over KZitem’s other coders cray man.
@Gringohuevon
5 жыл бұрын
gibberish
@money8330
5 жыл бұрын
🤔🤔But Still No cure for Parkinson's..... Disease
@jamma246
5 жыл бұрын
What a dumb comment.
@money8330
5 жыл бұрын
@@jamma246 NUMB brains can't understand my comments.
@money8330
5 жыл бұрын
@@jamma246 Can Mathematics cure Parkinson's disease which is a exponentially growing threat........🤔🤔🤔🤔
@dusanvuckovic17
5 жыл бұрын
hehe, he played with "coq" for two weeks. yes I am too dumb to understand Coq.
@money8330
5 жыл бұрын
🤔🤔But Still No cure for Parkinson's..... Disease
@Eric-u3v3r
Күн бұрын
Great! Your work might have much more profound implications. Now in 2024 AI can create average-quality research articles (in machine learning field), from conceptualization to implementation. With the creation of strong AI in the future, I see no reason that it can't invent new theories like human mathematicians. Formalizing math theories and defining things will make future AI able to do true mathematics (not something ambiguous in correctness).
@otakurocklee
5 жыл бұрын
It seems to me that at some point the journals should make this demand of mathematicians... submit computer proofs along with your papers. In the long run this will benefit everyone, but the mathematicians are currently not interested because they don't see the immediate benefit. But the reviewers will have an immediate benefit. How much easier it will be to review papers for correctness. I'd think math journals would be clamoring for this type of thing. I think this would speed up peer review. We have no structured database of knowledge... not even in mathematics... knowledge is scattered in raw text across the internet. What a waste. With computer formalization, all that knowledge can be synced and integrated. I think this approach would be valuable for all knowledge, not just mathematics. I really think this needs to be part of the journal process... so that our mathematics database remains immediately up to date... otherwise your going to have a backlog of papers that need formalization in the future.
@oblivion5683
5 жыл бұрын
This is a great comment and I think you're 100% correct. I think the work this guys doing is amazing and the computer formalization of mathematics will have tremendous benefits to the world.
@donaldviszneki8251
5 жыл бұрын
RE: "no structured database of mathematics" check out metamath.org. example proof in the database: us.metamath.org/mpeuni/aleph0.html
@andrepduarte
5 жыл бұрын
They aren't interested because it's not feasible to expect every maths professor and researcher to learn Lean or Coq or whatever. It's very difficult to formalise even a simple proof, let alone the kind of research-level mathematics these people are doing. Plus, these tools are under active development. Lean is what, one year old? It's just not feasible to make that a requirement. It might get there one day, but we're clearly not there yet.
@otakurocklee
5 жыл бұрын
@@andrepduarte I agree we aren't there yet. We need a high level language... something that is in between a formal proof, and a human proof.... that could be compiled down to a formal proof. The idea of ai actually being able to read and verify human-written math papers is ridiculous... The idea of mathematicians writing complete formal proofs is also ridiculous. We need something in between that a computer can compile.
@nihao19860630
5 жыл бұрын
Based on my personal experience, more and more mathematicians start to engage with computer science. The next generation of mathematicians must be proficient in programming. To convert the mathematical proof into the valid computer codes is a great idea and feasible to achieve in the long run.
@TheEtsgp1
5 жыл бұрын
Very informative! I will start looking into LEAN! I have a number theory proof I have been working on for 2 years. Python's types really can't handle the infinite number sets. This is very cool! Great Lecture!
@Blox117
5 жыл бұрын
best of luck in your proofs!
@TheEtsgp1
5 жыл бұрын
@@Blox117 Thank You!
@TheEtsgp1
5 жыл бұрын
@@emilywong4601 Awesome thank you very much!
@jamma246
5 жыл бұрын
_"Python's types really can't handle the infinite number sets"_ I'd suggest Haskell. If you know some category theory there are some really neat ideas in it inspired by category theory. Agda has an even more powerful type system. You may already know about these things of course.
@estmeta
5 жыл бұрын
could LEAN be used in math learning and question solving? I am learning abstract algebra in my spare time and feels really lonely and not sure if I got right the practice questions.
@ster2600
4 жыл бұрын
Yep definitely possible
@VasuJaganath
3 жыл бұрын
Yes, you can program proofs in Lean, I am sure Lean has packages for Monoids, Groups, Rings and Fields. Not sure about vector spaces though.
@funktorsound
3 жыл бұрын
@@VasuJaganath There seems to be definitions for linear algebra in mathlib leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html
@owenindri9897
5 жыл бұрын
I spent two weeks playing with coq - Kevin buzzard Dead 😂
@lonnybulldozer8426
5 жыл бұрын
I spent 50 years playing with coq. Many of my friends have dedicated their lives to playing with coq. For a lot of guys I know, they're no longer just playing with coq, coq is their life. They absolutely use coq to generate new things, and see what comes out of it. Sometimes they share what comes out of their coq with other coq enthusiasts. Sometimes it not easy, though, you really have to work at that coq. Sometimes you gotta get angry at that coq. Sometimes I get so mad, I give my coq a smack. Coq smack, I call it. I've literally pounded my coq, I got so mad. Some guys are very empathetic, and will pound other guys' coq for them. I don't do that, I just watch. It's pretty safe to say, that they're are coq lovers out there. Some are just coq-curious, while others are in coq denial. At the end of the day, I still get joy from playing with coq and the good stuff that eventually comes out of it.
@Neavris
5 жыл бұрын
@@lonnybulldozer8426 Coq: Initial release: 1 May 1989; 30 years ago (version 4.10)
@lonnybulldozer8426
5 жыл бұрын
@@Neavris What's your point?
@Neavris
5 жыл бұрын
@@lonnybulldozer8426 Obviously, the 50 years brag needs an explanation. Thierry Coqand isn't even 60. Are you 70? Just explain, plain and simple.
@lonnybulldozer8426
5 жыл бұрын
@@Neavris Oh, I get it. You're a moron. Unless a joke is graspable to a toddler, you're not going to get it. Even the slightest bit of subtlety will throw you off. You're the reason the world is not a pleasant place to be.
@VasuJaganath
5 жыл бұрын
Brilliant talk, the speaker has some very valid points about formalization and assisted proofs.
@gralha_
2 жыл бұрын
I've been using a programming language called Kind that supports theorem (and algorithms, they're isomophic through the curry-howard correspondence) proving. While it still lacks an automated theorem proof searcher, writing software and then writing proofs for it. Or writing proof for mathematical statements by writing them as algorithms and them proving it is really fun and really expanded my view on programing.
@drdca8263
5 жыл бұрын
What I’m kinda hoping for, is for a transpiler of sorts which can take a valid proof written in Lean and transform it into a valid proof of the same statement in Coq, and visa versa, and the same thing with HoL, etc. (Of course, because some of these don’t have quite the same foundations, not everything will translate right, but I imagine that all the main mathematical content will translate.) It would be **really** cool if, in addition to such a transpiler, we could have theorems saying that it could translate theorems provided that the proof has certain properties (like, not depending too much on the details of the foundation). Like, wouldn’t that be really cool? Then we could have our formal proofs relatively independent of the system we are using to prove. One person could prove something in Coq, another could automatically translate it to lean, and use it to prove something else in Lean, using the conclusion from the first proof, and then it could go back into Coq. Wouldn’t that be great!
@digama0
5 жыл бұрын
There are people who work in that area (I am one of them), but it's not that fashionable for some reason. Translating a theorem from system X to system Y usually results in a kind of garbage statement in system Y (it's not stated idiomatically and the proofs are probably very low level and unreadable), and there is usually a postprocessing stage where you turn the translated statements into the equivalent in the target system. You would not want to do this for the average theorem, because the overhead is probably higher than just proving it directly in system Y, but it might be good for the big name theorems with succinct statements like the odd order theorem. Translating between different dependent type theories is hard because definitional equality is finicky, but I have done a wholescale translation of the Metamath database to HOL and Lean.
@drdca8263
5 жыл бұрын
@@digama0 Woah, cool! When you say that it produces garbage statements, is that as like, the statement of the theorem, or just as the proof steps? I don't think I particularly mind the translated proof steps being not nice to read, as I've generally found proof system proofs to not be near as nice for reading as proofs designed primarily to be read by people (though, my sample size for that is small. Most of the ones I've seen have just been application of a few tactics.)? Like, if I'm already willing to sacrifice the aesthetic nice-to-read-ness of the proof by writing it a system like this in order to buy very high confidence in the correctness, I don't see making it even worse to read as losing much? But, if the _statement_ of the auto-translated proofs can be manually massaged into a nice enough form without too much effort (and still being able to use the translated proof), I think that still sounds very nice. So, what I mean to say by all that, is that I think what you are doing sounds really cool and impressive :)
@digama0
5 жыл бұрын
@@drdca8263 Usually both the statements and the proof come out pretty bad unless you work really hard to make them not-bad. The proofs usually end up worse than the statements though. Making the statements actually good usually requires human intervention, not necessarily a huge amount, but generally proportional to the size of the definitional stack leading to the statement of the theorem. For super advanced definitions like Kevin's perfectoid spaces that's not a trivial thing. The example I played with for Metamath -> Lean was to translate Dirichlet's theorem (on infinitely many primes in arithmetic progressions). Like Fermat's last theorem, the proof requires lots of advanced number theory but the statement is pretty simple, so it was reasonable to massage the statement that came out of the translation into the "idiomatic" way to state it in lean, using lean's natural numbers, lean's primes, and so on, rather than a bunch of statements about some model of ZFC inside lean (which has some set which is the translation of metamath's natural numbers, metamath's primes and so on).
@davidolsen1222
Жыл бұрын
Seems like the would-be turning point for theory-provers would be to prove an interesting mathematical theory in a way that most mathematicians wouldn't have the skills to access the proof but which is ultimately correct as proved by software. While something similar happened with the four-color theorem, it was proven by Appel and Haken but "confidence of the elders" was only solidified by the the computers, because it was basically a proof by exhaustion. You need a sort of, "you don't need the 'elders' it compiled, QED." moment. Currently the ABC conjecture is still believed solved in Japan but not outside of Japan, if the proof were formalized and compiled, it would certainly end the sort of screaming match issues that sort of turned the lecturer off from some level of human trust.
@apolloapostolos5127
5 жыл бұрын
23:31 * He’s thinking, “If I can do this I can do anything.” * I’m thinking, “If I could understand what he said, I could probably figure out why I’m so broke .”
@lucianoaraujo6604
5 жыл бұрын
Hahahaha
@NoNameAtAll2
5 жыл бұрын
As a student, this amazes me As physics student, I feel like everything is from outer world As a person interested in programming, this LEAN looks interesting to dig into But most important for me? The plan of presentation put on the side of the slide is the best invention I've seen and I'm going to -steal- use that
@cgibbard
5 жыл бұрын
I feel that it's very important, perhaps even moreso than for mathematics, that we find a way to do this for physics as well. A physical theory with an undetected logical inconsistency in it is more or less unfalsifiable (though it'll make individual claims which won't work so perhaps we'll find out that way). A lot of the mathematics which gets used by modern physics doesn't make it easy to turn a crank and get out predictions in a computable way. If physics could be formalized in something like dependent type theory in such a way that a significant portion of it was axiom-free, then the proofs of many theoretical results would be directly useful in computing numerical predictions. (They're literally computer programs which compute relevant things, even if not necessarily very efficiently.)
@makkabaion
5 жыл бұрын
His presentation is done in the latex beamer package, there is some style which does exactly this.
_"But most important for me? The plan of presentation put on the side of the slide is the best invention I've seen and I'm going to steal use that"_ I've seen a lot of beamer talks use that, don't worry about "stealing" it. IMO though, I think the best thing is to go completely minimal. The template for each slide should be blank. But that's just me.
@danthomas4198
2 жыл бұрын
Electrifying. Really generates enthusiasm.
@halian.vilela
6 күн бұрын
Coming here to happily tell, for those who thinks that someone who thinks like Kevin SHOULD be incentivized do keep going; that in 2024 he'd successfully got a grant to formalize Fermat's Last Theory in Lean!
@MikeKleinsteuber
5 жыл бұрын
Great stuff. Yet another part of the world where software is going to supersede humanity and leave us behind. Bring it on...
@ster2600
3 жыл бұрын
I think you underestimate the difficulty of this domain.
@dialecticalmonist3405
3 жыл бұрын
It's not going to leave "us" behind. It's going to interface with us. To what degree, is hopefully up to the individual.
@MikeKleinsteuber
3 жыл бұрын
@@dialecticalmonist3405 Likely to be true. The future of "us" is probably cyborg...
@dialecticalmonist3405
3 жыл бұрын
@@MikeKleinsteuber Book www.amazon.com/Artilect-War-Controversy-Concerning-Intelligent/dp/0882801546
@astroid-ws4py
Жыл бұрын
Software is written by groups/teams of humans so it is made up of the combined knowledge of many humans and this what makes it surepass the knowledge of the individual human.
@jamma246
5 жыл бұрын
This was an inspiring talk, well done Prof. Buzzard.
@thereGoMapo
5 жыл бұрын
Doron Zeilberger's book A = B has talked about this. Zeilberger's opinions on formal methods and criticisms in mathematics should be read more.
@tolkienfan1972
20 күн бұрын
"Can the too tell us anyhing new?" is a stupid question. The tool isn't a mathematician. Not yet. The question is "how does this tool help us?"
@woosix7735
5 ай бұрын
it's funny cause I think the thing where you can't sell formal proofs to british mathematicians in the "Gauss and Euler" tradition, I have a feeling that the same argument would have more sucsses in the Bourbaki influenced french tradition where they like to formalize quite a lot, and be realy sure that it math is founded on solid foundations.
@sajateacher
5 жыл бұрын
Did they have to call it Coq... just saying what everyone else is thinking...
@jamesh625
5 жыл бұрын
The French knew exactly what they were doing haha
@lopezb
5 жыл бұрын
@@jamesh625 Good point- I know other similar examples. Maybe it's the French getting back at prudish English and Americans! They put it in the terminology and can pretend innocence!!!
@drdca8263
4 жыл бұрын
Some people pronounce it like "coke" (which isn't the official pronunciation, but it is the pronunciation that I prefer)
@forranach
2 жыл бұрын
Where can i get that shirt?
@skylark4856
5 жыл бұрын
Logic programs have been around for a while. When it comes to proving theorems using computer logic that's a tall order. You effectively have to feed in an entire scaffolding of logic in order to set the context. This is before you can even begin to turn the handle to generate results. It's not surprising that MS is involved with this problem. They have a history in researching code completion in developer environments. A new project of theirs does the same thing but uses machine learning to cross reference instances of code from large pools of developer data. In fact if you look closely you might recognise, this is the same technology used in language translation on the Internet. The results aren't exactly spectacular but it gets the job done to a reasonable degree. I believe processes in contemporary machine learning are actually more mechanistic than heuristic. This is saying a lot when it comes to superimposing the notion to mathematical intuition in solving problems/proofs. Mathematical intuition is very much a human characteristic.
@ophello
5 жыл бұрын
Skylark the work in Gödel’s incompleteness theorem already showed that logic can be codified. I fail to see why it’s so hard to believe that tech could solve some of our deepest problems.
@dialecticalmonist3405
3 жыл бұрын
I agree. It's a greet tool, but reality itself is not a logical condition, it is an intuition. The limitations within the field of AI will slowly demonstrate that logic is not equal to reality.
@jmw1500
3 жыл бұрын
I am gonna call it now. "Computer Science" will be the new religious name people use when talking about formal discoveries. Mathematics will become like philosophy, that "unscientific" or "unrigorous" department on the other end of campus.
@DanielBWilliams
3 жыл бұрын
How can math be unrigorous ? We proove evrything we say.
@bttfish
3 жыл бұрын
@@DanielBWilliams That is the job left for the computers to complete. Mathematicians will only need to focus on discovering and inventing new theories which depends more on imagination than logical thinking.
@DanielBWilliams
Жыл бұрын
@@jmw1500 Knowing what kind of logic you need isn't really necessary to be rigourous.
@eelcohoogendoorn8044
5 жыл бұрын
Great talk. Mathematicians can learn so much from computer scientists when it comes to languages and tools. Computer scientists are forced to come up with languages that actually work in practice, solving real world problems together with other people. The design process of mathematical languages can roughly be characterised as 'what felt right to a guy perhaps centuries ago', and is devoid of any pragmatic feedback loops. The tendency of programmers to argue languages is sometimes derided; and they can be hung up on trivialities. But as a mathematician it also came as a shock to me when I realised most mathematicians seem actually opposed to any introspection as to what it is they are doing or how. Its a radically different culture. As someone who equally (little) identifies as either mathematican or computer scientist, I am very pleased for researchers to take the plunge into this scare interdisciplinary abyss. Actually writing down such an encyclopaedia of mathematics in a single sufficiently expressive language seems to me like an absolutely wonderful task. And for sure the process is going to teach us a lot of new things about mathematics and language itself. I get the impression that Lean isnt the last word in mathematical language when it comes to expressing high level mathematical reasoning; clearly human language is more expressive still, if formalizing in Lean feels comparatively tedious. If set-theoretic relations are like machine instructions, Lean feels more like C; not like what we would today consider a high-level programming language. And id be willing to bet it will not just reveal unstated assumptions, but also reveal subtle contradictions in widely held beliefs.
@aa888zz
5 жыл бұрын
>the design process of mathematical languages can roughly be characterised as 'what felt right to a guy perhaps centuries ago', No.
@money8330
5 жыл бұрын
🤔🤔But Still No cure for Parkinson's..... Disease
@eelcohoogendoorn8044
5 жыл бұрын
@@aa888zz Its a bit of a simplification; its language does of course undergo a slow cultural evolution. But insofar as there are people proactively thinking about what the language of mathematics ought to be, this is mostly an academic exercise; not something that impacts actual mathematicians, even over the centuries. Perhaps mathematicians are just better at getting it right the first time. But the fact that their language is either still too imprecise or too cumbersome for them to be able to write their own encyclopaedia in the sense discussed here, rather belies that notion.
@sadface7457
5 жыл бұрын
Algorithms are an applied mathmatics.
@tesset8828
5 жыл бұрын
@@money8330 Can you stop spamming this everywhere.
@lupercali3951
2 жыл бұрын
Great talk. Great pants.
@fbkintanar
3 жыл бұрын
Around 1:04:30, how does LEAN avoid setoid hell, if Coq doesn't? Is this something to do with making type classes available with quotient spaces? What does that even mean?
@ch2263
3 жыл бұрын
The coq people weren't happy about that comment. There's an axiom in Lean that lets you do quotients that could in principle be added to Coq but isn't. I think what they do instead is just use a type equipped with an equivalence relation instead of quotienting by the equality and using lemmas of the form x ~ y -> f(x) ~ f(y) whenever they need to make a substitution. This does indeed sound like hell.
@roys4244
5 жыл бұрын
The speaker was somewhat dismissive of Logic claiming that " it is all checked and OK". However these computer based proof systems are going to be based on a Constructive Logic, as a result some theorems may not quite "say" what they say in the standard mathematical literature. Even Set Theory (which he was also somewhat dismissive of) will be formalised in a Constructive way (and thus be a different theory). The Foundational Framework in use here is a form of (Dependent) Type Theory. In some mathematical areas, perhaps including Combinatorics and Number theory, many proofs are (essentially) constructive, though it is tedious to dot the i's and cross all the t's as he seems to be saying - hence a proof tool is helpful there.. My understanding is that many of these proof tools were originally developed by Computer Scientists to assist with combinatorially tedious and error prone tasks in Formal Software Engineering. The corresponding Foundational Type theories could fit well there. However to convince Mathematicians in general of their overall validity I think that he will need to spend some time clarifying the foundational differences - including any foundational differences between Coq and Lean etc. There are discussions of these kind of topics in the Constructive Mathematics literature, and I think he will have to refer to that in future.
@alexbest8905
5 жыл бұрын
I'm not sure what you mean here; Lean is not purely constructive? It has the option of using classical logic, and this is used all the time in the lean maths library. Can you elaborate what you mean by this?
@roys4244
5 жыл бұрын
@@alexbest8905 Hi. I have just read the Lean PDF "Logic and Proof" which answers most of my points above. I did not necessarily intend to criticize Lean, just this presentation did not give me what I would have wanted to see. So Lean does have a Prop type which helps encode two valued logic, and the document does confirm the other points I made and discusses the link (in outline) between Lean's Type theory and ZFC Set Theory. As the document points out there are some subtleties because Lean is ultimately constructive (e.g. the Ex elimination rule needs a value of the given type to be pre-declared). There are further questions to be answered though: what about higher ZF axioms (ie doing ZF research in Lean); what about declaring another Logic (e.g. Modal logic); the proof of some non-constructive theorems (the Model Existence theorem was mentioned in the document as "tricky"). The Speaker did say that he learned new things trying to prove results using Lean, and I guess that these issues were in there.
@etdr
3 жыл бұрын
those pants tho
@IKnowNeonLights
10 ай бұрын
(International philosophers project) Theorems conditions. International philosophers project are and have to be the same thing as a standing on their own. If and when put together are and have to become different. International on its own is all encompassing. Philosophers on its own is all encompassing. Project on its own is all encompassing. (International philosophers project), as one statement is not (is not meant or taken as) all encompassing, it refers to three different structural group types which if and when put together become a different group type. Yet by always being exactly the same thing as three different types, quantum probabilistic predictions can be derived at pleasure under all circumstances exactly as with and within the none quantum states. Sigma is/= X,Y,Z no matter what, how or when. Bell is wrong, all bells are wrong. In fact forget all what is written before this sentence and use only the sentence (Bell is wrong, all bells are wrong), and that very sentence shows Bell's inequality theorem to be wrong, as clearly as the very statement Bell is wrong, all bells are wrong, which in itself is a theorem that obeys preset conditions and a, any and possible combinations of quantum probabilistic predictions can be derived at pleasure with and within all possible conditions from, for, by, off, and to it.
@jesseburstrom5920
5 жыл бұрын
The expectation theorem, what is the next move?!
@yogeshchavan2503
5 жыл бұрын
IF..U..have any.. machine .. capable ..of.. creating..it's..own.. Evolution.. Matrix..then that machine has its own self..!! Now how to write Evolution Matrix code....it's problem to you by me ??
Пікірлер: 320