![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Formalizing invisible mathematics: case studies from higher category theory
![]() Formalizing invisible mathematics: case studies from higher category theoryAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact nobody. BPRW03 - Big proof: formalizing mathematics at scale One thing that quickly becomes clear when attempting to formalize recent mathematical discoveries in a computer proof assistant is how much “invisible mathematics” is obscured in a proof on paper. This talk will attempt to present a taxonomy of the various forms of invisible mathematics that have been made visible by attempts to formalize higher category theory. We then describe specific challenges inherent to large-scale formalization projects that are exacerbated by invisible mathematics. This talk is part of the Isaac Newton Institute Seminar Series series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsPDN TALKS Opzionibinarie Numerical AnalysisOther talksCanine Myasthenia Gravis: Insights from 167 cases and the need for better diagnostics Thermal shift methods and high throughput screening Instructing the imagination : the role of place in mathematical training Enriched enumerative geometry via equivariant homotopy theory From “Green Revolution” to “Economic Liberalization” in 1970s-80s' India: Impacts of Oil Crises in a Global Perspective External Seminar - Michael Rassig TBC |