[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Emily Riehl is this year’s Hardy lecturer, sponsored by the London Mathematical
Society. She is touring the UK and her talks are listed here:
https://urldefense.com/v3/__https://www.lms.ac.uk/events/lectures/hardy-lectureship*Hardy*20Current__;IyU!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9UhxYkUwg$
On Wednesday 2 July at 11:00 she is speaking in Birmingham (title and abstract
below), followed by a lunch reception. To register for this free event, please
register at
https://urldefense.com/v3/__https://forms.cloud.microsoft/e/mjghTazu5h__;!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9UbcCuLOo$
After lunch, there will be an Assume meeting:
https://urldefense.com/v3/__https://tdejong.com/ASSUME/__;!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9Ucc6cFmc$
Best regards,
Paul
--
Prospects for formalizing the theory of weak infinite-dimensional categories
Emily Riehl (Johns Hopkins University)
Over the past several years, mathematicians have launched increasingly
ambitious computer formalization projects targeting increasingly complex areas
of mathematics. This talk will present a high level case study involving
∞-category theory. A peculiarity of the ∞-categories literature is that proofs
are often written without reference to a concrete definition of the concept of
an ∞-category, a practice that creates an impediment to formalization. We
describe three broad strategies that would make ∞-category theory formalizable,
which may be described as “analytic,” “axiomatic,” and “synthetic.” We then
highlight two parallel ongoing collaborative efforts to formalize ∞-category
theory in two different proof assistants: the “axiomatic” theory in Lean and
the “synthetic” theory in Rzk. We show some sample formalized proofs to
highlight the advantages and drawbacks of each approach and explain how you
could contribute to this effort.
