HGS MathComp - Where Methods Meet Applications
The Heidelberg Graduate School of Mathematical and Computational Methods for the Sciences (HGS MathComp) at Heidelberg University is one of the leading graduate schools in Germany focusing on the complex topic of Scientific Computing. Located in a vibrant research environment, the school offers a structured interdisciplinary education for PhD students. The program supports students in pursuing innovative PhD projects with a strong application-oriented focus, ranging from mathematics, computer science, bio/life-sciences, physics, and chemical engineering sciences to cultural heritage. A strong focus is put on the mathematical and computational foundations: the theoretical underpinnings and computational abstraction and conception.
HGS MathComp Principal Investigators are leading experts in their fields, working on projects that combine mathematical and computational methodology with topical research issues. Individual mentoring for PhD candidates and career development programs ensure that graduates are fully equipped to take up top positions in industry and academia.
11.11.2026
16:30 - 18:00
16:30 - 18:00
Theory & Methods
"Machine learning galore!" Scientific Machine Learning
Colloquium
Location: Mathematikon • 5th Floor • Im Neuenheimer Feld 205 • 69120 Heidelberg
Registration: Please register via this form • Please register for free by November 9th!
Organizer: MLAI
Registration: Please register via this form • Please register for free by November 9th!
Organizer: MLAI
ECTS: 1 for 5
Machine learning galore will feature lab presentations by PIs as well as scientific talks by junior scientists.
To help plan the catering, please register for free by clicking here.
Scientific Machine Learning is a joint initiative from STRUCTURES and IWR aimed at fostering interactions within and development of the local machine learning community. Its portal summarizes the many relevant events and news from across campus that would otherwise remain scattered across single institutions or fields. The goals of the MLAI platform align with the STRUCTURES Cluster of Excellence's objective of driving research into the fundamental understanding of current and future machine learning, and with IWR’s aim to leverage machine learning to enable the solution of long-standing problems in the natural and life sciences, the engineering sciences, as well as the humanities.
Further information and links:
MLAI homepage • Machine Learning Talks on Campus – Information service and mailing list • STRUCTURES Cluster of Excellence
To help plan the catering, please register for free by clicking here.
Scientific Machine Learning is a joint initiative from STRUCTURES and IWR aimed at fostering interactions within and development of the local machine learning community. Its portal summarizes the many relevant events and news from across campus that would otherwise remain scattered across single institutions or fields. The goals of the MLAI platform align with the STRUCTURES Cluster of Excellence's objective of driving research into the fundamental understanding of current and future machine learning, and with IWR’s aim to leverage machine learning to enable the solution of long-standing problems in the natural and life sciences, the engineering sciences, as well as the humanities.
Further information and links:
MLAI homepage • Machine Learning Talks on Campus – Information service and mailing list • STRUCTURES Cluster of Excellence
Lab presentations
Lena Maier-Hein • Claudia Strauch • Alexander Zipf
Rocket science
Leon Mayer (Maier-Hein Lab)
How Naturally Adverbial Medical Images Challenge Vision-Language Models
Marta Gentiloni Silveri (Strauch Lab)
How Reliably Can Generative Models Reconstruct Data from Pure Noise?
Gefei Kong (Zipf Lab)
From bird’s eyes to human eyes: mapping street-view greenness by DL model from satellite imagery and geo foundation embeddings
Lena Maier-Hein • Claudia Strauch • Alexander Zipf
Rocket science
Leon Mayer (Maier-Hein Lab)
How Naturally Adverbial Medical Images Challenge Vision-Language Models
Marta Gentiloni Silveri (Strauch Lab)
How Reliably Can Generative Models Reconstruct Data from Pure Noise?
Gefei Kong (Zipf Lab)
From bird’s eyes to human eyes: mapping street-view greenness by DL model from satellite imagery and geo foundation embeddings
12.11.2026
- 13.11.2026
10:00 - 16:00
10:00 - 16:00
Theory & Methods
Interactive Theorem Proving in Lean
Compact Courses
Speaker: Prof. Dr. Florent Schaffhauser • Institute for Mathematics, Heidelberg University
Location: Mathematikon • Conference Room, Room 5/104, 5th Floor • Im Neuenheimer Feld 205, 69120 Heidelberg
Registration: Please register via this form • Registration open until November 5, 2026
Organizer: HGS MathComp
Location: Mathematikon • Conference Room, Room 5/104, 5th Floor • Im Neuenheimer Feld 205, 69120 Heidelberg
Registration: Please register via this form • Registration open until November 5, 2026
Organizer: HGS MathComp
ECTS: 1
An 8h introduction to certified programming and formal mathematics for graduate students interested in the interaction between mathematics and computer science.
Course times on both days: 10:00 - 12:00 & 14:00 - 16:00
What is Lean?
Introduced by Leonardo de Moura in 2013, Lean is an open-source functional programming language that can be used as an interactive theorem prover. In this workshop, we will see it in action as a development environment for computer-assisted mathematics.
Course times on both days: 10:00 - 12:00 & 14:00 - 16:00
What is Lean?
Introduced by Leonardo de Moura in 2013, Lean is an open-source functional programming language that can be used as an interactive theorem prover. In this workshop, we will see it in action as a development environment for computer-assisted mathematics.
Course description
Producing certified, reliable code is crucial in software engineering. Taking it a step further, modern programming languages with strong type-checking capabilities can even be used to state theorems about abstract mathematical objects and verify the correctness of proofs.
In this workshop, we will explore the world of proof assistants and learn how to explain mathematics to a computer using Lean. The goal is to help participants develop new coding skills while becoming acquainted with formal methods on a larger scale.
Contents of the workshop
The course will consist of four 2-hour sessions, spread over two days. Each session will combine a lecture with hands-on computer practice. Please bring your laptop.
- Lecture 1: Basic Lean syntax
- Lecture 2: Tactics
- Lecture 3: Dependent types
- Lecture 4: Group project
Participants will be asked to work in pairs. The instructor will provide practice files for each session and no prior installation of Lean is required.
Producing certified, reliable code is crucial in software engineering. Taking it a step further, modern programming languages with strong type-checking capabilities can even be used to state theorems about abstract mathematical objects and verify the correctness of proofs.
In this workshop, we will explore the world of proof assistants and learn how to explain mathematics to a computer using Lean. The goal is to help participants develop new coding skills while becoming acquainted with formal methods on a larger scale.
Contents of the workshop
The course will consist of four 2-hour sessions, spread over two days. Each session will combine a lecture with hands-on computer practice. Please bring your laptop.
- Lecture 1: Basic Lean syntax
- Lecture 2: Tactics
- Lecture 3: Dependent types
- Lecture 4: Group project
Participants will be asked to work in pairs. The instructor will provide practice files for each session and no prior installation of Lean is required.
12.11.2026
16:15 - 17:15
16:15 - 17:15
Theory & Methods
Mathematical Colloquium: On Covering Numbers
Colloquium
Speaker: Prof. Dr. Kai Cielieback • Augsburg
Location: Mathematikon • Lecture Hall, Ground Floor • Im Neuenheimer Feld 205 • 69120 Heidelberg
Registration: No registration required
Organizer: Institute for Mathematics
Location: Mathematikon • Lecture Hall, Ground Floor • Im Neuenheimer Feld 205 • 69120 Heidelberg
Registration: No registration required
Organizer: Institute for Mathematics
ECTS: 1 for 5
The purpose of the Mathematical Colloquium is the local and international exchange on current research topics from various fields of mathematics. The talks start, during the semester and alternating weekly with the IWR Colloquium on Scientific Computing, always on Thursdays at 16h c.t. in the Hörsaal Mathematikon.
Following the merger of the (now former) two mathematical institutes in Heidelberg to a single Institute for Mathematics, the Mathematical Colloquium is intended in particular to further promote the exchange between pure and applied mathematics. All six sections of the Institute contribute to the diverse program, so that it reflects the entire breadth of mathematics in Heidelberg. Speakers are asked to make their talk accessible to a broad audience and ideally to offer a motivation at Master's level at the beginning, so that our students can also benefit from the colloquium.
Following the merger of the (now former) two mathematical institutes in Heidelberg to a single Institute for Mathematics, the Mathematical Colloquium is intended in particular to further promote the exchange between pure and applied mathematics. All six sections of the Institute contribute to the diverse program, so that it reflects the entire breadth of mathematics in Heidelberg. Speakers are asked to make their talk accessible to a broad audience and ideally to offer a motivation at Master's level at the beginning, so that our students can also benefit from the colloquium.
For a radius r, the r-covering number of a compact metric space is the smallest number of r-balls covering the space. The following (apparently new) conjecture generalizes Vizing's conjecture from graph theory: The r-covering number of a product, equipped with the maximum metric, is greater or equal to the product of the r-covering numbers.?I will provide two pieces of evidence for this conjecture. First, it holds if one of the spaces is a metric graph. Second, its infinitesimal version for r-covering numbers of Finsler manifolds with very small r follows from known results about covering densities by convex sets.