You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Jun 30 2021 at 14:50):Thursday the 1st of July (tomorrow) at 17:00 UTC
Abstract:
A long-standing question in mathematics is the relevance of formalisation to practice. Rising awareness of fallibility among mathematicians suggests formalisation as a remedy. But are today's proof assistants up to the task? And what is the right formalism?
A wide variety of mathematical topics have been formalised in simple type theory using Isabelle/HOL. The partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly technical results were obtained by Erdös-Milner, Specker and Larson (among many others) for the case of ordinal partition relations, which is concerned with countable ordinals and order types. Much of this material was formalised last year (with the assistance of Džamonja and Koutsoukou-Argyraki).
Grothendieck's Schemes have also been formalised in Isabelle/HOL. This achievement is notable because some prominent figures had conjectured that schemes were beyond the reach of simple type theory.
Some highlights of this work will be presented along with general observations about role of type theory in the formalisation of mathematics.
Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=Znh3UlUrek41T3RLQXJVRVNkM3Ewdz09
YouTube: https://www.youtube.com/watch?v=tYqbbRsx8DI
Tim Hosgood (Jul 01 2021 at 16:58):starting in 3 minutes!
Rich Hilliard (Jul 01 2021 at 21:58):During Lawrence Paulson's talk, there was a note in the chat (alas, I missed the poster's name):
"The Edinburg school (Rod Burstall-David Rydeheard-Tatsuya Hagino) has attempted intrinsic Computational Categorical Datatypes; and the school of Kosta Dosen goes farther with intrinsic Computational-Logic Categorical Datatypes with Sheafification (the MODOS proof-assistant). Have you reviewed these attempts?"
I'm familiar with the works of Burstall, Rydeheard and Hagino, but I've never heard of MODOS. Google was unhelpful, but for one cryptic page. Does anyone have a reference?
Peter Arndt (Jul 02 2021 at 04:04):I guess the cryptic page was this one? There is this link to a github repository where there is a pdf (all pdfs there seem to be identical) giving some hints at what MODOS is. But it's not a real explanation. I guess if you can read Coq better than me you can get more out of it...
Rich Hilliard (Jul 02 2021 at 10:13):Yes, that is the cryptic page and link to repository that I found. I've downloaded the Coq files for study ;-)