Math Talk! Dr Kevin Buzzard, Langlands, diversity, and proof assistants.

In this interview I chat with Dr. Kevin Buzzard about Langlands, diversity and getting more women in mathematics, and proof assistants, particularly Lean.
The natural number game: www.ma.imperial.ac.uk/~buzzar...
Lean community:
leanprover.github.io/
Introduction & journey to math (0:00)
The path to Langlands (9:28)
Privilage, luck, and (a lack of) diversity (15:36)
Lean & proof assistants (28:55)
Pedagogy of assistants (42:28)
I butcher HoTT (55:32)
A HoTT challenge (1:23:49)
Where's it going? (1:27:00)
A useless fiction (1:34:10)

Пікірлер: 13

  • @alvarol.martinezruiz5077
    @alvarol.martinezruiz5077 Жыл бұрын

    Kevin was my undergraduate "personal tutor" as they call it at Imperial. We would have meetings where he would explain things that would largely go over my head. However our discussions left a long-lasting influence on me, especially as an algebraist. He also veered me away from contest problems, and into actual math. I feel privileged to have had him then, and I'm quite sure I wouldn't be where I am now without him.

  • @jackozeehakkjuz
    @jackozeehakkjuz Жыл бұрын

    Thanks for this charming conversation. So great!

  • @k-theory8604

    @k-theory8604

    Жыл бұрын

    Glad you enjoyed it :)

  • @maryammahmoudigharaie
    @maryammahmoudigharaie Жыл бұрын

    Enjoyed the talk on diversity and including minorities (women here in particular)

  • @k-theory8604

    @k-theory8604

    Жыл бұрын

    Glad you enjoyed it! On hand I feel a little silly, because the last thing the topic needs is some white dudes like Kevin and I chiming in on the topic; but on the other, I think it's precisely because we come from such advantaged backgrounds that we have these discussions, and are mindful to create a more equitable future.

  • @tanchienhao
    @tanchienhao Жыл бұрын

    agree that it should be made easier! i am a programmer but type theory still confuses me alot

  • @k-theory8604

    @k-theory8604

    Жыл бұрын

    I'm not sure that type theory itself can be made much easier. It is a foundation for mathematics after all! That being said, one thing we can always improve on is pedagogy.

  • @tanchienhao

    @tanchienhao

    Жыл бұрын

    @@k-theory8604 definitely! Resources on leanprover is quite sparse (or rather hard to navigate), I’d definitely make videos on it once I understand, but sadly the learning curve is very hard for me and my friend to climb without consistent help

  • @k-theory8604

    @k-theory8604

    Жыл бұрын

    @@tanchienhao Be sure to let me know when/if you put some videos out there! It's been on my mind to make more proof assistant content, but there's only so many hours in the day :p

  • @lexinwonderland5741
    @lexinwonderland5741 Жыл бұрын

    (commenting while watching) I think math olympiads don't make mathematicians, they make brilliant engineers and financial analysts, but not mathematicians because they don't address the fundamental part of maths. Other STEM fields require rapidly applying known problem solving, or using a non-math field to find a solution to a math(like) problem; mathematics is about the fundamentals of problem solving and relating patterns in formal language. Mathematics mastery comes from far slower, longer projects than the variety of intense problem solving that appears in other STEM or applied-maths-related fields.

  • @k-theory8604

    @k-theory8604

    Жыл бұрын

    Well that's certainly true, but I think we should be careful not to over-demonize the Olypmiads as well. I do like the analogy that Olympiads are learning to sprint, when mathematics is more of a marathon. And, unfortunately, some would-be mathematicians have a hard time transitioning after competitions... At the same time, I also have a number of friends who have benefitted from the connections they made through participating in competitions. And, it's probably not just a coincidence that a lot of the famous names in modern mathematics have gold medals in their track record. I would also argue that engineers and analysists can and often do benefit from being slow and deep thinkers, just as much as mathematicians. And hey, if you do some very spceific analysis and/or combinatorics, it can be helpful to have a lot of weird tricks memorized! TL;DR: Everything in balance.