Towards a Semantic Language of Mathematics
Why MathOverflow recommends it
MathOverflow users link it as a documentary on formalizing mathematics, both in the "Interesting mathematical documentaries" thread and when discussing proof assistants and the status of informal proofs.
Recommended by 1 people across 1 different months, 2016 to 2021.
What it is
A documentary-style film from Wolfram about computerizing pure mathematics, built from interviews and talk segments recorded at a Sloan Foundation workshop on semantic representation of mathematical knowledge at the Fields Institute in 2016. It features mathematicians, logicians, computational mathematicians and theorem-prover experts, and was scripted and produced by Amy Young and Michael Trott.
What people said
Recommends Witiko · 2021-10 · MathOverflow · on “Interesting mathematical documentaries”
Thank you, I much enjoyed the recording and I will reference your workshop in my upcoming dissertation on math information retrieval. As a token of my gratitude, I posted a table of contents for people who would like to get a quick overview of the recording: [this video]
Cites Michael Trott · 2016-12 · MathOverflow · on “Interesting mathematical documentaries”
In February of this year (2016), the Alfred P. Sloan Foundation sponsored a workshop at the Fields Institute about the development of a new 'language' to represent mathematics in computerized/formalized form. The participants were 40 mathematicians, logicians, experts in computational mathematics and formalized mathematics. Because bringing the approximate 100 million pages of peer-reviewed research mathematics into a modern, computer-understandable form will be a long term global effort ( [LINK] ), the Alfred P. Sloan Foundation also sponsored the making of a documentary-style video about the workshop; including participant interviews (e.g. with Ingrid Daubechies, Yuri Matiyasevich, Harvey
Cites Mei Zhang · 2018-01 · MathOverflow · on “Proofs shown to be wrong after formalization with proof assistant”
I'm aware that I'm trusting things developed by others such as software and hardware, but we have a sensible notion of when these things have bugs and are therefore wrong and should to be fixed. To me this notion is a bit more unclear when we talk about informal math. Maybe at this point I am actually being too pedantic, but let me share this video which I think is relevant to the discussion. In particular, the talk between 43:24 and 44:25 which touches on the "not even wrong" argument: [this video]