<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-2022-jp">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;
panose-1:2 11 0 4 2 2 2 2 2 4;}
@font-face
{font-family:"Open Sans";
panose-1:2 11 6 6 3 5 4 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Aptos",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
span.MsoSmartlink
{mso-style-priority:99;
color:blue;
background:#F3F2F1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Aptos",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:11.0pt;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="#467886" vlink="#96607D" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">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:<o:p></o:p></p>
<p class="MsoNormal"><a href="https://urldefense.com/v3/__https://www.lms.ac.uk/events/lectures/hardy-lectureship*Hardy*20Current__;IyU!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9UhxYkUwg$">https://www.lms.ac.uk/events/lectures/hardy-lectureship#Hardy%20Current</a><o:p></o:p></p>
<p class="MsoNormal">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
<o:p></o:p></p>
<p style="margin:0cm;background:white"><span style="font-size:10.5pt;font-family:"Open Sans",sans-serif;color:#333333"><a href="https://urldefense.com/v3/__https://forms.cloud.microsoft/e/mjghTazu5h__;!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9UbcCuLOo$"><span class="MsoSmartlink">https://forms.cloud.microsoft/e/mjghTazu5h</span></a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">After lunch, there will be an Assume meeting:
</span><a href="https://urldefense.com/v3/__https://tdejong.com/ASSUME/__;!!IBzWLUs!VkTevsuEiXAtejfkz-5WtH6eQdmw9K2pyf3a1_XF_MB9SvakDofPsWcnwpSjjDYqUgbGrFW0Y5-HMw_7Fcg_9KS5Lu9Ucc6cFmc$"><span style="font-size:10.5pt;font-family:"Open Sans",sans-serif;color:#038ABA;background:white;text-decoration:none">https://tdejong.com/ASSUME/</span></a><o:p></o:p></p>
<p class="MsoNormal">Best regards,<o:p></o:p></p>
<p class="MsoNormal">Paul<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">--<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Prospects for formalizing the theory of weak infinite-dimensional categories<o:p></o:p></p>
<p class="MsoNormal">Emily Riehl (Johns Hopkins University)<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>