Introducing: The Annals of Formalized Mathematics afm.episciences.org/ The AFM is a @oa_math -supported diamond open access overlay journal. It publishes original articles about formalized mathematics and mathematical applications of proof assistants, spanning many proof assistant ecosytems. Papers should be written for an audience of mathematicians and should not focus on the details of the tools themselves. Papers do not necessarily need to present novel mathematical proofs but should describe the mathematical lessons learned during the formalization process. Please keep the AFM in mind when you write up your next project, and help us spread the word! Scientific advisory board Jeremy Avigad, Carnegie Mellon University, Pittsburgh, PA (United States) Georges Gonthier, INRIA Saclay Île-de-France, Palaiseau (France) Timothy Gowers @wtgowers, Collège de France, Paris (France) and Trinity College, Cambridge (United Kingdom) Tom Hales, University of Pittsburgh, Pittsburgh, PA (United States) Sophie Morel, CNRS, École Normale Supérieure de Lyon (France) Editorial board Antoine Chambert-Loir @achambertloir, Université Paris-Cité (France) Manuel Eberl, University of Innsbruck (Austria) Sébastien Gouëzel, CNRS, IRMAR Rennes (France) Alex Kontorovich, Rutgers University, Piscataway, NJ (United States) Marco Maggesi, Università di Firenze (Italy) Assia Mahboubi, INRIA Nantes (France) Colleen Robles, Duke University, Durham, NC (United States) Managing editors Robert Y. Lewis, Brown University, Providence, RI (United States) Filippo A. E. Nuccio Mortarino Majno di Capriglio, Université Jean Monnet Saint-Étienne (France)