post · 8 October 2026
Verification was never just about certification
What to check before trusting “verified in Lean”, why it adds little to AI-generated proofs, and what formal code is actually good for.
Combinatorialist working on AI for Mathematical Discovery
Christoph Spiegel
Deputy head of AIS²T
at ZI
An extremal combinatorialist by training, I like to describe my approach as computational thinking: formalize problems to make them approachable through computational tools and AI.
Current & upcoming
course · winter 2026/27
Formal Proof Verification (BSc/MSc)
A two-week intensive course on formalized mathematics in Lean 4 taught at FUB / ZIB as part of the BMS program. Vorlesungsverzeichnis
event · 13 November 2026 – 14 November 2026
Kolloquium über Kombinatorik
I am organizing the 2026 iteration of KolKom at TUB’s IMoS with plenary talks by Maria Axenovich, Matthew Kwan, Monique Laurent, and Mohit Singh.
public talk · 2026-11-17
Do Machines Dream of Colored Planes?
BMS/MATH+ Celebration Ceremony · Berlin
Recent papers
C14
Fast Isotopy Computation for T-Curves
J16
An Unsure Note on an Un-Schur Problem
J15
The four-color Ramsey multiplicity of triangles
J14
The Rado multiplicity problem in vector spaces over finite fields
C13
Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transformers
P7
Limits of combinatorial patchworking
Recent talks
Überschwemmt mit KI-generierten Beweisen: Was ist die Zukunft der Mathematik?
Mathenacht Aus Berlin, Bonn Und Münster Online
With Thomas NikolausThoralf Räsch (Moderator)Peter Scholze
Trust, but Verify: Formal Proof Verification with Lean
IOL @ Speinshart Scientific Center for AI and SuperTech ZIB Speinshart
Fast Isotopy Computation for \(T\)-Curves
Conference on Discrete Optimization and Machine Learning Tokyo
Coloring the Plane with Neural Networks
Coloring the Plane with Neural Networks
IBS Extremal Combinatorics and Probability Group IBS Daejeon
An Unsure Talk on an Un-Schur Problem
Flags in the Mountains Bellvue
Latest from Appendix
-
Verification was never just about certification
What to check before trusting “verified in Lean”, why it adds little to AI-generated proofs, and what formal code is actually good for.
Event organization
13 November 2026 – 14 November 2026
Kolloquium über Kombinatorik
Organizer
The 2026 iteration of the annual German combinatorics colloquium at TUB’s IMoS with support from ZIB and MATH+. Plenary talks will be given by Maria Axenovich, Matthew Kwan, Monique Laurent, and Mohit Singh.
19 August 2026 – 21 August 2026
TIBOR - A Colloquium on Extremal and Probabilistic Combinatorics
Organizer
With Letícia Mattos
A Colloquium on Turán Numbers, Intersections, Biased Games, Orientations, and Ramsey Graphs. Plenary talks were given by Penny Haxell, Michael Krivelevich, Anita Liebenau, Mathias Schacht, and Gábor Tardos. The colloquium celebrated Tibor Szabó’s 60th birthday.
16 July 2026 – 18 July 2026
FoCM 2026: Graph Theory and Combinatorics
Co-organizer
With Kurusch Ebrahimi-Fard, Claudia Malvenuto
A workshop at FoCM 2026 in Vienna. Talks were given by Christian Krattenthaler, Stephanie van Willigenburg, Aida Abiad, Manuel Bodirsky, Loïc Foissy, Jan Hladký, Andrey Boris Khesin, Daniel Kráľ, Svante Linusson, Hong Liu, Arnau Padrol, Oleg Pikhurko, Pascal Schweitzer, Elizabeth Xiao, Alexandra Wesolek, and Hanmeng Harmony Zhan.
3 July 2024 – 5 July 2024
Discrete Mathematics Days
Session chair
Earlier events
11 June 2024 – 13 June 2024
ZIB40 2024: ZIB Forty - Past and Future
Session chair
A series of scientific and public events celebrating the 40th anniversary of the Zuse Institute Berlin.
2024
40 Years Zuse Institute Berlin
Organizing committee member
A series of scientific and public events celebrating the 40th anniversary of the Zuse Institute Berlin.
10 February 2023 – 15 September 2023
MATH+ Thematic Einstein Semester: Mathematical Optimization for Machine Learning
Organizing committee member
A MATH+ semester on mathematical optimization for machine learning, with three workshops, a summer school, and a final conference.
7 November 2022
Festkolloquium for Martin Aigner
Assisting organizer
A colloquium celebrating Martin Aigner’s 80th birthday at ZIB. Mathias Schacht, Emo Welzl, and Günter M. Ziegler gave lectures.
6 September 2021 – 10 September 2021
European Conference on Combinatorics, Graph Theory and Applications
Organizing committee member · Online
The European Conference on Combinatorics, Graph Theory and Applications, held online.
10 June 2019 – 11 June 2019
Postgraduate Combinatorial Conference
Session chair
9 October 2017 – 10 October 2017
BMS-BGSMath Junior Meeting
Organizing committee member
The first joint meeting of the Berlin and Barcelona graduate schools in mathematics, with keynote lectures and short talks by the participants.
15 July 2016 – 16 July 2016
Symposium Diskrete Mathematik
Organizational support
June 2016
Discrete Mathematics Days
Organizational support
Outreach organization
6 June 2026
Lange Nacht der Wissenschaften at ZIB
Coordinator for IOL contributions
6 June 2026
Ein Bild, unendliche Welten: Von Gemälden bis Galaxien (LNdW at ZIB 2026)
Booth organizer
With Berkant Turan
Interactive generative-AI photo booth: visitors transform their own portrait into historical, futuristic, or imaginary scenes and different artistic styles.
6 June 2026
Geometrische Färbungen: Das Hadwiger-Nelson Problem (LNdW at ZIB 2026)
Booth organizer
With Konrad Plato
Touchscreen coloring game about the chromatic number of the plane. Visitors arrange points to find colorings with as few unit-distance conflicts as possible.
28 June 2025
Ein Bild, unendliche Welten: Von Gemälden bis Galaxien (LNdW at ZIB 2025)
Booth organizer
With Berkant Turan
Interactive generative-AI photo booth: visitors transform their own portrait into historical, futuristic, or imaginary scenes and different artistic styles.
Earlier events
28 June 2025
Geometrische Färbungen: Das Hadwiger-Nelson Problem (LNdW at ZIB 2025)
Booth organizer
With Konrad Plato
Touchscreen coloring game about the chromatic number of the plane. Visitors arrange points to find colorings with as few unit-distance conflicts as possible.
22 June 2024
Ein Bild, unendliche Welten: Von Gemälden bis Galaxien (LNdW at ZIB 2024)
Booth organizer
With Berkant Turan, Konrad Plato, Max Zimmer
Interactive generative-AI photo booth: visitors transform their own portrait into historical, futuristic, or imaginary scenes and different artistic styles.
17 June 2023
Bilder mit ML verändern (LNdW at ZIB 2023)
Booth helper
Interactive image-generation demonstration using Stable Diffusion and InvokeAI.
28 April 2022
Girls' Day at FUB 2022: Spielen wie die Mathematiker*innen
Workshop organizer · Online
With Olaf Parczyk, Simona Boyadzhiyska, David Fabian, Tatiana Levinson, Patrick Morris, Shagnik Das, Evgeniya Lagoda
Workshop on tic-tac-toe, Nim, and related positional games, introducing the mathematical ideas behind winning strategies.
22 April 2021
Girls' Day at FUB 2021: Zufall und menschliche Intuition
Workshop organizer · Online
With Simona Boyadzhiyska, Giulia Codenotti, Shagnik Das, Patrick Morris, David Fabian
Interactive probability puzzles exploring how human intuition can misjudge randomness, including the Monty Hall problem.
Posters
I like to design the occasional conference or event poster. Click on each poster to get a full view or an overview of its variants.