What are...computer proofs?

Goal.
I would like to tell you a bit about my favorite theorems, ideas or concepts in mathematics and why I like them so much.
This time.
What are...computer proofs? Or: Who needs mathematicians?
Disclaimer.
Nobody is perfect, and I might have said something silly. If there is any doubt, then please check the references.
Slides.
www.dtubbenhauer.com/youtube.html
TeX files for the presentation.
github.com/dtubbenhauer/My-Te...
Thumbnail.
Picture from cmartinez.web.wesleyan.edu/do...
Main discussion.
en.wikipedia.org/wiki/Categor...
formalabstracts.github.io/
cmartinez.web.wesleyan.edu/do...
www.ams.org/notices/202011/rn...
www.ams.org/notices/200811/tx...
www.quantamagazine.org/how-cl...
math.stackexchange.com/questi...
arxiv.org/abs/math/9404236
link.springer.com/article/10....
www.nature.com/articles/d4158...
www.jstor.org/stable/2025805
sites.math.washington.edu/~bi...
link.springer.com/book/10.100...
calculemus.org/MathUniversali...
Background material.
en.wikipedia.org/wiki/Proof_a...
en.wikipedia.org/wiki/Automat...
en.wikipedia.org/wiki/Compute...
en.wikipedia.org/wiki/Automat...
en.wikipedia.org/wiki/Artific...
en.wikipedia.org/wiki/Mathema...
en.wikipedia.org/wiki/Compute...
en.wikipedia.org/wiki/Formal_...
en.wikipedia.org/wiki/Compute...
Computer talk.
en.wikipedia.org/wiki/Categor...
reference.wolfram.com/languag...
Pictures used.
www.qedcat.com/misc/noword3.jpg
e7.pngegg.com/pngimages/577/7...
Picture from • What is...the Jordan c...
Pictures from cmartinez.web.wesleyan.edu/do...
KZbin and co.
• Thomas Hales: Formal A...
• Georges Gonthier: Comp...
#logic
#computerscience
#mathematics

[@ThomasFackrell]

This makes me very excited! This absolutely needs to be the future of mathematics

[@VisualMath]

It is exciting, yes 😄 But the state of the arts is not as good as it could be - so let us all work to improve it together ✌

[@ThomasFackrell]

@@VisualMath are you involved with any of the people who wrote the book on HoTT?

[@VisualMath]

@@ThomasFackrell No, sadly not as I come from a different area of math

[@chavita4321]

What would you call the field of computer science (or math?) that formalizes theorems for computers to prove?

[@VisualMath]

That is an excellent question. I would personally sort this into mathematical logic, but people might disagree. This also is part of homotopy type theory, artificial intelligence and symbolic computation (and many more that I am forgetting right now).

[@sequentcalc]

automated reasoning, perhaps

[@VisualMath]

@@sequentcalc Right that makes sense, but I would count that as part of AI. But again, this is just my personal take.

[@arslanrozyjumayev8484]

i think "Formal Methods in Software design" is the answer to your question, i might be wrong, though!

[@VisualMath]

@@arslanrozyjumayev8484I like that one! But I still feel like there is no single correct answer, but many correct answers. And that is nothing negative.