Jeremy Avigad: "Formal mathematics, dependent type theory, and the Topos Institute"

4th of November, 2021. Part of the Topos Institute Colloquium.
-----
Abstract: Modern logic tells us that mathematics can be formalized, in principle. Computational proof assistants, developed over the last half century, make it possible to do so in practice. In this talk, I will briefly survey the state of the field today and discuss some of the reasons that formalization is desirable. I will discuss one particular proof assistant, Lean, and its library, mathlib. I will explain why dependent type theory, Lean's underlying logical framework, provides an attractive platform for formalization. Finally, I will consider ways that formal mathematics can support and enhance the Topos Institute's missions.

[@NoNTr1v1aL]

I LOVE LEAN!!! Great video btw.

[@rinosanchez2150]

I think that even top research mathematicians could be interested in formalizing mathematical results that don’t come from recent research. Just look at the Bourbaki group and their books building up many fields in math from basic foundations. They were all top mathematicians of the time, and I think this approach to formalizing mathematics would have been of great interest to many of them.

[@encapsulatio]

Is there a book(or multiple books) that's considered gold standard for learning all the logic necessary in type theory that is used in different papers on gradual types, dependent types?
Thank you!

[@valeriadepaiva8390]

well, there are several collections, but nothing I feel like singling out right now. will try to think about it, thanks for the question!

[@encapsulatio]

@@valeriadepaiva8390 It would help if professors would not wait to teach students about formal logic until university.
For example you can find open source curriculums that gives an outline of computer science education you can use to self learn computer science by yourself but what I found so far is pretty generic and has formal logic as an afterthought.
For learning formal logic and make that my priority I have not found any resources.
Sure there are many books out there only known by academics but no one guides you what to learn and in what order. It would be nice if you who has focused so much on logic could make the field accessible to middle school and high school students. Or write a in depth blog with what resources we need to self study ourselves. Thank you very much!

[@valeriadepaiva8390]

@@encapsulatio agree a 100% that it would help! will try to produce a blog post about it!

[@encapsulatio]

@@valeriadepaiva8390 I will monitor logic forall blogspot for that new blog post. Thank you again!