(I am posting this in my capacity as chair of the ICM programme committee.)
ICM 2022 will feature a number of "special lectures", both at the sectional and plenary level, see last year's report of the ICM structure committee. The idea is that these are lectures that differ from the traditional ICM format (author of a recent breakthrough result talking about their work). Some possibilities are
- a Bourbaki-style lecture where a recent breakthrough result (or series of results) is put into a broader context,
- a "double act" where related results are presented by two speakers,
- a survey lecture on a subfield relevant for some recent development,
- a lecture that doesn't fit into any of the existing sections,
- a lecture creating new connections between different areas of mathematics,
but these are not meant to be exhaustive in any way. So what special lecture(s) would you like to see at the next ICM?
(Unless it is self-evident, please state what makes the lecture you would like to see "special". If you would like to nominate someone for an "ordinary" plenary lecture instead, please do so by sending me an email.)
Best Answer
How about a lecture on proof assistants/formal proofs?
Most mathematicians are still skeptical of the value of proof assistants, and it's certainly true that proof assistants are still very difficult for the average mathematician to use. However, I think that much of the skepticism stems from a lack of understanding of what proof assistants have to offer. A popular misconception is that proof assistants just give you a laborious way of increasing your certainty of the correctness of a proof from 99% to 99.9999%. But that's not where their primary value lies, IMO.
For example, having a large body of formalized mathematics available could help machine learning algorithms figure out what constitutes "interesting" mathematics and help them autonomously discover interesting new definitions and concepts—something that seems beyond what computers can do now. For another example, there are increasingly many cases where editors can't find a referee for a complicated and potentially important paper because the referees are skeptical and don't want to waste time studying something that might be wrong. If proof assistants become sufficiently easy to use that authors are routinely required to formally verify their proofs before submission, then referees can focus on the more rewarding work of assessing whether a result is interesting and important instead of spending the bulk of their time checking correctness.
A good lecture on this topic could give the subject a valuable boost. Incidentally, if you want to poll people to assess interest, I would recommend polling younger people. This is one topic where I would value the opinion of younger mathematicians and students more than the opinion of senior mathematicians.