About the Lectureship:
The LMS Hardy Lectureship is named after G.H. Hardy, former President of the Society and De Morgan Medallist. Originally awarded to a distinguished overseas mathematician in odd-numbered years.
The LMS Hardy Lecturer visits the UK for a period of about two weeks, and gives the Hardy Lecture at a Society meeting, normally held in London in July. The LMS Hardy Lecturer also gives at least six other lectures, on different topics, at other venues in the UK; the schedule is decided by the LMS Society, Lectures and Meetings Committee in consultation with the LMS Hardy Lecturer, and is designed to allow as many UK mathematicians as possible to benefit from the LMS Hardy Lecturer's presence in the UK.
The 2025 Hardy Lecturer is Emily Riehl. Professor Riehl has established herself as a leading expert in higher category theory and has also developed an interest in connections with computer science such as homotopy type theory. She is an accomplished and enthusiastic expositor of mathematics at a variety of levels aimed at mathematicians as well as popular writing with articles in Scientific American and New Scientist. She also plays a leading role in broader engagement of mathematicians and other scientists from marginalized and discriminated against groups.
For the full list of events, please click here: https://www.lms.ac.uk/events/lectures/hardy-lectureship
Programme:
Speakers:
Emily Riehl (Johns Hopkins University)
Title: Prospects for formalizing the theory of weak infinite-dimensional categories
Abstract: 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.
Please note that speakers and timings are subject to change.
Accessibility:
For accessibility details on this room, please click here: https://servicenow.bham.ac.uk/lrat?id=centrally_managed_rooms&spa=1&sys_id=2c3146bc37b3920056d1d1b543990ebd
Registration:
To register for this free event, please contact Paul Levy (p.b.levy@bham.ac.uk).
Travel/Caring Grants to attend the Hardy Lectures:
Travel/Caring grants of up to £50 to support attending the Hardy Lectures, which are at universities on the Hardy Lecture Tour, were available to mathematicians who are based at neighbouring universities to those universities and would require financial support.
For future Hardy Lecture Tours, if you require support, please complete the application form as soon as you can and at least 3 working days before the Hardy Lecture you wish to attend. Please note that there are limited funds available and so grants may be awarded on a first-come, first-served basis.
If you have any queries, please email lmsmeetings@lms.ac.uk