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.
Jean-Baptiste Vienney (Oct 12 2023 at 04:07):I have a question concerning the trimester Prospects of formal mathematics on May - August 2024 at the HIM. (Probably for @Valeria de Paiva and @Jacques Carette ) To apply we need to write a 1-4 pages letter of intent describing the research projects we want to work on during the stay. Is it supposed to be research only on formal mathematics?
They say also concerning the trimester "At the same time the goal is to provide a platform for junior researchers to enter Formal Mathematics." This is why I would want to come: to enter formal mathematics. But I don't have research projects in formal mathematics now even if I could think to a few things but not very precise. I can describe research projects on the kind of math I'm doing but it's not exactly research on formal mathematics. It's very formal and probalby very formalizable, but not "formal mathematics" per se.
Jean-Baptiste Vienney (Oct 12 2023 at 04:09):Now I remember, I was a bit afraid by this point the first time I looked at the website.
Valeria de Paiva (Oct 12 2023 at 14:35):hi @Jean-Baptiste Vienney , I think you write exactly what you just said above in the application, plus the formalizable research you're already doing and if possible which routes you envisaged using: which prover, how do you intend to go about it, who do you want to talk to, etc.. caveat:I've never being to a HIM program so this is just my gut feeling, as I'm also finding very difficult to discover how things work there.
Jacques Carette (Oct 13 2023 at 14:32):Indeed: we haven't been told that much from HIM. I think this is just the standard way they do it. At the end of the day, I believe it will be the organizers who choose, so we're the audience to aim for.
Jean-Baptiste Vienney (Oct 13 2023 at 15:31):Ok, thank you both!
Steve Awodey (Oct 21 2023 at 17:01):not to make too much of the coincidence of names, I think the area of "formal category theory" is a natural one for formalization projects: the theory of 2-categories is (dependently typed) algebraic, so 2-categorical axiomatics of higher categorical structures can be formalized in a "cold" proof assistant like Lean. If someone would start a project like this on GitHub that others could join, there would be plenty of work for people to do - more than enough for a working group at the Hausdorff Trimester. Another possibility would be a project using the new Rzk proof assistant being developed by @Emily Riehl , @Jonathan Weinberger , and @Nikolai Kudasov -- but I'll let one of them fill you in on that!
Jean-Baptiste Vienney (Oct 21 2023 at 17:15):I was thinking to 2-categorical structure in some way me too. I'm going to propose to formalize cut elimination for logical systems based on the structures in the theory of differential categories: differential categories, cartesian differential categories, tangent categories. That's more a niche subject that formal category theory. But I 100% agree with your proposal :+1:
Emily Riehl (Oct 21 2023 at 17:17):Steve Awodey said:
not to make too much of the coincidence of names, but I think the area of "formal category theory" is a natural one for formalization projects: the language of 2-categories is algebraic, so 2-categorical axiomatics of higher categorical structures in can be formalized in a "cold" proof assistant like Lean. If someone would start a project like this on GitHub that others could join, there would be plenty of work for other people to do - more than enough for a working group at the Hausdorff Trimester. Another possibility would be a project using the new Rzk proof assistant being developed by Emily Riehl , Jonathan Weinberger , and Nikolai Kudasov -- but I'll let one of them fill you in on that!
Indeed I mentioned this as a proposed collaborative project (in Lean) in my Letter of Intent for the trimester program. I think it would be relatively accessible to newcomers.
Jonathan Weinberger (Oct 22 2023 at 01:42):Thanks @Steve Awodey! We do invite contributions and collaborations on rzk's sHoTT library, see the GitHub pages:
https://github.com/rzk-lang/sHoTT
Of course, the Hausdorff trimester would be a great venue to work on this.