| Wed | Jan 14 | 07:30 | Moscow-Beijing topology seminar | Natalia V. Maslova | On Gruenberg-Kegel graphs and beyond | |
| Wed | Jan 14 | 11:00 | ICCUB Seminars | Thomas Celora | Modelling bulk-viscotiy in NS mergers: hydrodynamic challenges | |
| Wed | Jan 14 | 11:30 | RA Seminar | Nicholas Williams | The talk has been postponed to 8 April. | |
| Wed | Jan 14 | 13:00 | SISSA's Analysis seminars | Federico Renzi | The superposition principle for local 1-dimensional currents | |
| Wed | Jan 14 | 15:00 | AnLy Strings and Fields online seminars | Alek Bedroya | Holographic Constraints on the String Landscape | |
| Wed | Jan 14 | 15:00 | Port-Hamiltonian Seminar | Karim Cherifi | System identification of port-Hamiltonian systems | |
| Wed | Jan 14 | 16:00 | FGC-HRI-IPM Number Theory Webinars | Kübra Benli | Sums of proper divisors with missing digits | |
| Wed | Jan 14 | 17:00 | Metagovernance Seminar | No seminar | TBA | |
| Wed | Jan 14 | 23:00 | University of Utah Representation Theory / Number Theory Seminar | Shenghao Li | Base change fundamental lemma for Bernstein centers of principal series blocks | |
| Thu | Jan 15 | 13:00 | Geometric Structures Research Seminar | Andrei Agrachev | Geometry of osculating curves | |
| Thu | Jan 15 | 15:00 | Quantum Theories of Fields, Matter, and Strings | Alison Warman | Phases with Generalized Symmetries from the SymTFT | |
| Thu | Jan 15 | 15:00 | Seminar on Analysis, Differential Equations and Mathematical Physics | Maxim Shishlenin | Wave tomography: theory, numerical methods and neural networks | |
| Thu | Jan 15 | 16:00 | Number Theory Web Seminar | Daniel Loughran | Arithmetic statistics via algebraic stacks | |
| Thu | Jan 15 | 19:00 | Online logic seminar | Gilda Ferreira | From Commuting Conversions to Syntactic Identity | |
| Thu | Jan 15 | 21:30 | SFU NT-AG seminar | Felix Thimm | Wall-Crossing and the DT/PT3 Descendant Correspondence | |
| Fri | Jan 16 | 08:00 | Nagoya Math-Phys Seminar | Vincent Caudrelier | Classical Yang-Baxter equation, Lagrangian multiforms and ultralocal integrable hierarchies | |
| Fri | Jan 16 | 14:15 | Symplectic zoominar | Oliver Edtmair (ETH) | On the topological invariance of helicity | |
| Fri | Jan 16 | 16:00 | CRM - Séminaire du CIRGET / Géométrie et Topologie | Jérôme Vétois | Nonexistence of extremals for the second conformal eigenvalue in low dimensions | |
| Fri | Jan 16 | 16:00 | GEOTOP-A seminar | Ivan Smalyukh | Artificial matter from knots: solitons and vortices in chiral media | |
| Fri | Jan 16 | 20:30 | FirstPrinciples Talks | Chenhao Tan | Science in the Age of AI | |
| Sat | Jan 17 | 14:05 | Knots, graphs and groups | Zihao Liu | TBA | |
| Mon | Jan 19 | 11:30 | Basic Notions and Applied Topology Seminar | Jacek Gulgowski | Linear Model Selection and Regularization (Part 2) | |
| Mon | Jan 19 | 12:15 | CAM seminar | Start | TBA | |
| Mon | Jan 19 | 13:00 | Paris algebra seminar | Markus Reineke | Varieties of complexes and canonical bases of quantum groups | |
| Mon | Jan 19 | 14:00 | Lean Together 2026 | Lean Together Organizers | Opening Remarks | |
| Mon | Jan 19 | 14:15 | Lean Together 2026 | Johan Commelin | The Mathlib Initiative: Scaling, Infrastructure, and Future Directions | |
| Mon | Jan 19 | 14:40 | Nečas Seminar on Continuum Mechanics | semester break | TBA | |
| Mon | Jan 19 | 14:45 | Lean Together 2026 | Vasilii Nesterov | Verified computation of real asymptotics | |
| Mon | Jan 19 | 15:00 | European Non-Associative Algebra Seminar | Dimitar Grantcharov | U(h)-Free sl(2)-Modules of rank 2 | |
| Mon | Jan 19 | 15:00 | Geometric and functional inequalities and applications | Detang Zhou | Eigenvalue estimate on self shrinkers | |
| Mon | Jan 19 | 15:15 | Lean Together 2026 | Jonas van der Schaaf | Internal Projectivity of the Sequence Space in Lean | |
| Mon | Jan 19 | 15:45 | Lean Together 2026 | Break | Break | |
| Mon | Jan 19 | 16:00 | Lean Together 2026 | Leopoldo Sarra | Towards autoformalization for physics and engineering with Lean | |
| Mon | Jan 19 | 16:30 | Lean Together 2026 | Yaël Dillies | Hopf algebras, affine group schemes and all of that | |
| Mon | Jan 19 | 17:00 | Lean Together 2026 | Break | Break | |
| Mon | Jan 19 | 17:30 | Lean Together 2026 | Leo de Moura | The State of Lean | |
| Mon | Jan 19 | 18:30 | Lean Together 2026 | Siddharth Bhat | Sound & Complete Tactics for the Linear-Bitwise Fragment of Multi-Width Parametric Bitvector Theory | |
| Tue | Jan 20 | 00:00 | Fraser Valley Math & Stats Seminar | Tariq Nuruddin | Akaike's Information Criteria for comparison of statistical models | |
| Tue | Jan 20 | 06:00 | OIST representation theory seminar | Pavel Turek | Balanced columns of decomposition matrices | |
| Tue | Jan 20 | 12:30 | Lean Together 2026 | Moritz Doll | Formalizing Schwartz functions and tempered distributions | |
| Tue | Jan 20 | 13:00 | Lean Together 2026 | Fabrizio Montesi | CSLib: The Lean Computer Science Library | |
| Tue | Jan 20 | 13:30 | Lean Together 2026 | María Inés de Frutos Fernández | Formalizing the universal divided power algebra | |
| Tue | Jan 20 | 14:00 | One World Combinatorics on Words Seminar | Savinien Kreczman | Factor complexity and critical exponent of words in a Thue-Morse family | |
| Tue | Jan 20 | 14:00 | One world IAMP mathematical physics seminar | Holger Gies | Quantum field theories of relativistic Luttinger fermions | |
| Tue | Jan 20 | 14:00 | Lean Together 2026 | Break | Break | |
| Tue | Jan 20 | 14:30 | Lean Together 2026 | Sebastian Ullrich | The Lean module system | |
| Tue | Jan 20 | 15:00 | Lean Together 2026 | Stefan Kebekus | Project VD: Formalizing Value Distribution Theory of Complex Analysis | |
| Tue | Jan 20 | 15:30 | Lean Together 2026 | Break | Break | |
| Tue | Jan 20 | 16:00 | International seminar on automorphic forms | Katy Woo | TBA | |
| Tue | Jan 20 | 16:00 | Lean Together 2026 | Sebastian Graf | Simpler $\texttt{do}$ proofs with $\texttt{mvcgen}$ | |
| Tue | Jan 20 | 16:00 | Potomac region PDE seminar | Anping Pan | Variational principle and Lagrangian formulations of hydrodynamic equations | |
| Tue | Jan 20 | 16:30 | Lean Together 2026 | David Ledvinka | Formalization of Brownian Motion in Lean | |
| Tue | Jan 20 | 17:00 | Lean Together 2026 | Harry Goldstein | Metaprogramming the Next Generation of Testing Tools | |
| Tue | Jan 20 | 19:30 | NHETC Seminar | Nathan Seiberg | Symmetry, Anomaly, Gauging, Proliferation, and Condensation | |
| Tue | Jan 20 | 21:00 | UCLA analysis and PDE seminar | Luccas Campos | Scattering for the k-DgBO | |
| Tue | Jan 20 | 23:30 | PIMS-CORDS SFU Operations Research Seminar | Nicholas Richardson | Optimization and applications for unsupervised signal demixing | |
| Wed | Jan 21 | 07:30 | Moscow-Beijing topology seminar | Andreani Petrou | TBA | |
| Wed | Jan 21 | 09:30 | NCTS international Geometric Measure Theory seminar | Paul Minter | Stationary Integral Varifolds near Multiplicity 2 Planes | |
| Wed | Jan 21 | 10:00 | AUTH HEP-TH Seminars | Gerben Oling | TBA | |
| Wed | Jan 21 | 12:15 | Gothenburg statistics seminar | Simon Olsson | Transferable Implicit Transfer Operators | |
| Wed | Jan 21 | 16:00 | Lean Together 2026 | Markus Himmel, Sofia Rodrigues | TBA | |
| Wed | Jan 21 | 16:30 | Lean Together 2026 | Break | Break | |
| Wed | Jan 21 | 17:00 | Lean Together 2026 | Jovan Gerbscheid | New tools for theorem proving in Lean | |
| Wed | Jan 21 | 17:00 | Metagovernance Seminar | Cecilia Rikap | "Intellectual Monopolies" in the AI Age (Understanding Control Beyond Ownership) | |
| Wed | Jan 21 | 17:00 | Topological Quantum Field Theory Club (IST, Lisbon) | Maxine Calle | Nested cobordisms and TQFTs | |
| Wed | Jan 21 | 17:30 | Lean Together 2026 | Sophie Morel | TBA | |
| Wed | Jan 21 | 18:00 | Lean Together 2026 | Break | Break | |
| Wed | Jan 21 | 18:30 | Lean Together 2026 | Thomas Murrills | Skimmer: A Cotool For Library-Scale Change | |
| Wed | Jan 21 | 19:00 | Lean Together 2026 | Sidharth Hariharan, Seewoo Lee, Chris Birkbeck | Progress on the Sphere Packing Project | |
| Wed | Jan 21 | 19:30 | Lean Together 2026 | Break | Break | |
| Wed | Jan 21 | 20:00 | Lean Together 2026 | Alex Kontorovich | Teaching Real Analysis as a Video Game | |
| Wed | Jan 21 | 20:30 | Lean Together 2026 | Chris Henson | Proof Automation and Metaprogramming in CSLib: Locally Nameless Lambda Calculi | |
| Thu | Jan 22 | 14:15 | Real and complex Geometry | Andres Franco Valiente | Introduction to tropical-topological (tropological) sigma models | |
| Thu | Jan 22 | 15:00 | Lean Together 2026 | Wojciech Różowski | Coinductive predicates in Lean | |
| Thu | Jan 22 | 15:30 | Lean Together 2026 | Oliver Dressler | lean-lsp-mcp: Tools for agentic interaction with Lean | |
| Thu | Jan 22 | 16:00 | Lean Together 2026 | Break | Break | |
| Thu | Jan 22 | 16:00 | Number Theory Web Seminar | Lillian Pierce | Counting points in thin sets: a big picture | |
| Thu | Jan 22 | 16:30 | Lean Together 2026 | Hannah Scholz | Formalisation of CW complexes | |
| Thu | Jan 22 | 17:00 | Lean Together 2026 | Salvatore Mercuri | Foundations for FLT: Topological structure and base change for the adele ring | |
| Thu | Jan 22 | 17:30 | Lean Together 2026 | Etienne Marion | Formalization of the Ionescu-Tulcea theorem in Mathlib | |
| Thu | Jan 22 | 18:00 | Lean Together 2026 | Julius Marx | MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL in Lean | |
| Thu | Jan 22 | 19:00 | Online logic seminar | Adrian Mathias | TBA | |
| Fri | Jan 23 | 08:00 | SEU Yau Center Theoretical Physics Seminars | Pratik Rath | TBA | |
| Fri | Jan 23 | 13:00 | Analysis Junior Seminars | Guglielmo Padula | TBA | |
| Fri | Jan 23 | 13:00 | Lean Together 2026 | Kim Morrison | TBA | |
| Fri | Jan 23 | 13:30 | Lean Together 2026 | Alex Best | TBA | |
| Fri | Jan 23 | 14:00 | Lean Together 2026 | Son Ho | Formal Verification of Rust Cryptographic Code in Lean with Aeneas | |
| Fri | Jan 23 | 14:15 | Symplectic zoominar | Levin Maier (Heidelberg); Elad Kosloff (HUJI); Joel Schmitz (Neuchâtel) | Three 20min research talks | |
| Fri | Jan 23 | 14:30 | Lean Together 2026 | Break | Break | |
| Fri | Jan 23 | 15:00 | Lean Together 2026 | Christoph Thiele | TBA | |
| Fri | Jan 23 | 15:30 | Lean Together 2026 | Michal Mrugala | Formalizing Class Field Theory | |
| Fri | Jan 23 | 16:00 | Lean Together 2026 | Break | Break | |
| Fri | Jan 23 | 16:30 | Lean Together 2026 | Joël Riou | Formalization of homotopy theory in Lean | |
| Fri | Jan 23 | 17:00 | Lean Together 2026 | Atticus Kuhn | Verification of model-checking techniques in Lean | |
| Sat | Jan 24 | 14:05 | Knots, graphs and groups | Oleg German | TBA | |
| Mon | Jan 26 | 08:00 | Tropical mathematics and machine learning | Assaf Shocher | TBA | |
| Mon | Jan 26 | 12:15 | CAM seminar | Mihaly Kovacs | TBA | |
| Mon | Jan 26 | 13:00 | Paris algebra seminar | Fan Qin | Quantum cluster algebras over commutative rings and quantized coordinate rings of simple algebraic groups | |
| Mon | Jan 26 | 14:40 | Nečas Seminar on Continuum Mechanics | semester break | TBA | |
| Mon | Jan 26 | 15:00 | European Non-Associative Algebra Seminar | Bernardo Leite da Cunha | TBA | |
| Mon | Jan 26 | 15:00 | Geometric and functional inequalities and applications | Fausto Ferrari | Recent regularity results in free boundary problems | |
| Mon | Jan 26 | 15:00 | SISSA algebraic geometry seminar | Giordano Crimi | Derived categories of cubic 4-folds. I | |
