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:
Speaker: Emily Riehl (Johns Hopkins University)
Title: Path induction and the indiscernibility of identicals
Abstract. Mathematics students learn a powerful technique for proving theorems about an arbitrary natural number: the principle of mathematical induction. This talk introduces a closely related proof technique called path induction, which can be thought of as an expression of Leibniz's indiscernibility of identicals: if two objects are identified, then they must have the same properties, and conversely. What makes this interesting is that the notion of identification referenced here is given by Per Martin-Löf's intensional identity types, which encode a more flexible notion of sameness than the traditional equality predicate in that an identification can carry data, for instance of an explicit isomorphism or equivalence. The nickname "path induction" for the elimination rule for identity types derives from a new homotopical interpretation of type theory, in which the terms of a type define the points of a space and identifications correspond to paths. In this homotopical context, indiscernibility of identicals is a consequence of the path lifting property of fibrations. Path induction is then justified by the fact that based path spaces are contractible.
Please note that speakers and timings are subject to change.
Accessibility:
Details TBC
Registration:
To register for this free event, please contact Enrico Pajer (enrico.pajer@gmail.com)
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