4 ms·

The Type Theory Forall podcast published an interview this week with Kevin Buzzard who has been coordinating the mathlib efforts[1] for Lean. If you're interest

by nequo 4y ago

The Type Theory Forall podcast published an interview this week with Kevin Buzzard who has been coordinating the mathlib efforts[1] for Lean. If you're interested in math, theorem provers, or Lean, then it is worth listening to: https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard.html https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard... [1] https://leanprover-community.github.io/ https://leanprover-community.github.io/

kevinbuzzard 4y ago
Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I think it has the potential to change mathematics. But it is coordinated by many people, like many open source projects.
- deterministic 4y ago
  Thanks for doing the interview Kevin. I have learned a lot from your articles and interviews over the years. Especially how different the math I care about (computation) is from the math that mathematicians care about (structure). It is great to see that with Lean/mathlib computer scientists and mathematicians have found a way to work together and benefit from the insights and skills of each other. So please continue doing what you are doing. I believe it will long term have a massive positive impact on both computer science and mathematics.
deterministic 4y ago
Thanks! I just listened to it. What a great interview. It made me realise yet again that the math used by computer scientists is usually different from the math used by mathematicians. Because what computer scientists care about (computations and proofs) is very different from what mathematicians care about (structures and proofs). Which means that computer scientists often choose a different foundation for the mathematics they use. Set theory is but one possible foundation. However other foundations (based on type theory for example) are more useful for computer scientists. Resulting in a different flavour of mathematics. And things that are proven to be true in one foundation isn’t necessarily true in another foundation. However it is all still math. Just different flavours of math based on different foundational axioms.

by nequo 4y ago

kevinbuzzard 4y ago

Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I think it has the potential to change mathematics. But it is coordinated by many people, like many open source projects.

deterministic 4y ago
Thanks for doing the interview Kevin. I have learned a lot from your articles and interviews over the years. Especially how different the math I care about (computation) is from the math that mathematicians care about (structure). It is great to see that with Lean/mathlib computer scientists and mathematicians have found a way to work together and benefit from the insights and skills of each other. So please continue doing what you are doing. I believe it will long term have a massive positive impact on both computer science and mathematics.

deterministic 4y ago

Thanks! I just listened to it. What a great interview. It made me realise yet again that the math used by computer scientists is usually different from the math used by mathematicians. Because what computer scientists care about (computations and proofs) is very different from what mathematicians care about (structures and proofs). Which means that computer scientists often choose a different foundation for the mathematics they use. Set theory is but one possible foundation. However other foundations (based on type theory for example) are more useful for computer scientists. Resulting in a different flavour of mathematics. And things that are proven to be true in one foundation isn’t necessarily true in another foundation. However it is all still math. Just different flavours of math based on different foundational axioms.