Workshops and conferences [conf]

You will find me in the following incoming activities:

Conference. STRATIFYING KIEL: Stratified Spaces from Higher Category Theory to Applied Topology [kiel_2026_stratify]

Stratified spaces have proven themselves to be a rich and ubiquitous class of mathematical objects, with appearances in diverse areas such as classical algebraic and differential topology and geometry, higher category theory and topological data analysis. With this conference, we aim to foster the exchange of recent advances, ideas and methods between these various communities, working on and with stratified spaces.

Conference. Non-archimedean methods in arithmetic and tropical geometry [fra_2026_non_archimedean]

Conference. CATS 8 - A conference in honour of Gabriele Vezzosi’s 60th birthday [cnrs_2026_cats8]

Conference. Arithmetic Geometry and Higher Algebra - A conference on the occasion of Lars Hesselholt’s 60th birthday [ch_2026_ag_ha]

I have participated in:

Conference. Young Topologists Meeting 2026 [ch_2026_ytm]

Workshop. Kleine AT II - Topological cyclic homology [wuppertal_2026_kat]

A one-day workshop series for early‑career algebraic topologists in NRW and neighboring regions.

Workshop. Lean Workshop 2025 : Formalising Algebraic Geometry [heidelberg_2025_fag]

I formalized lemmas regarding geometrically irreducibility of a ring, and its relation to tensor products. And shown this coincides with the same notion in scheme world.

This workshop is aimed primarily at PhD students with an interest in formalising results from algebraic geomery using the Lean proof assistant. Participants will work in teams on formalisation projects designed by our guest speakers.

Conference. Higher Invariants: interactions between arithmetic geometry and global analysis [regensburg_2025_hi]

Workshop. CMI-HIMR summer school on formalizing class field theory [oxford_2025_cmi]

The Github repo is: kbuzzard/ClassFieldTheory.

I formalized part of Tate cohomology and local fields.

Class Field Theory in its cohomological form is one of the highlights of early 20th century mathematics, and is now understood as the abelian case of the Langlands Philosophy. Although it sounds like science fiction to many mathematicians, some computer scientists are arguing that AI methods are progressing so fast that soon computers will be helping humans to push back the boundaries of research in the Langlands Philosophy. However, there is currently no concrete evidence that this is happening. Furthermore, using a language model alone to do mathematics at this level is problematic, because language models are error-prone, and one error in a mathematical argument invalidates it.

This summer school does not have anything to do with AI, but it has a lot to do with class field theory. During the school, we will be teaching class field theory to the Lean theorem prover. You can imagine the school as a group of people collaborating on writing a Bourbaki-like document explaining class field theory. Or you can imagine it as a group of people turning class field theory into a bunch of levels of a puzzle game and then solving these levels. Or you can imagine it as a group of people creating training data for a theorem prover-backed AI which can then try and learn some of these interesting mathematical ideas.

Conference. Graduate Research Opportunities for Women 2025 [fra_2025_GROW]

GROW@Frankfurt 2025 is for all students of underrepresented gender identities in mathematics, especially female students, who are interested in learning about graduate programmes and further opportunities in research, both within and outside academia.