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.
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.
17.11.2026
09:00 - 17:00
09:00 - 17:00
Theory & Methods
The Unix Shell + Version Control with Git
Compact Courses
Speaker: James Bowyer, Research Software Engineer, Scientific Software Center (SSC)
Location: Mathematikon • Conference Room • Im Neuenheimer Feld 205, 69120 Heidelberg
Registration: Please register on the course website
Organizer: Scientific Software Center (SSC)
Location: Mathematikon • Conference Room • Im Neuenheimer Feld 205, 69120 Heidelberg
Registration: Please register on the course website
Organizer: Scientific Software Center (SSC)
ECTS: 0.5
This is a one day course. The first half of the day covers the basics of the Unix Shell, the second half covers Version Control with Git.
The latest information and a registration link are available on the course website.
This compact course is part of the course program of the Scientific Software Center (SSC) at Heidelberg University.
The latest information and a registration link are available on the course website.
This compact course is part of the course program of the Scientific Software Center (SSC) at Heidelberg University.
Prerequisites:
No prior knowledge by the participants is necessary to participate in this course and it is intended for all scientific audiences. Participants are required to bring their own laptops to work on during the course. Network access (e.g. through Eduroam) is recommended.
Summary:
The Unix shell is a powerful tool that allows people to do complex things with just a few keystrokes. More importantly, it helps them combine existing programs in new ways and automate repetitive tasks so they aren’t typing the same things over and over again. Use of the shell is fundamental to using a wide range of other powerful tools and computing resources. The course will include hands-on live coding sessions where participants exercise the learned commands on their own computers.
Version control is the lab notebook of the digital world: it is used to keep track of what was done and to collaborate with other people. Its use is the state of the art in software development projects of all scales. However, it is not limited to software: books, papers, small data sets, and anything that changes over time or needs to be shared can and should be stored in a version control system. The course will include hands-on live coding sessions where participants exercise the learned commands on their own computers.
Learning Objectives:
After this course the participants will
- Have a fundamental understanding of how and why to use the Unix Shell
- Be comfortable with handling files and directories using the command line
- Have experience with advanced usage of the shell e.g. loops, pipes, redirects etc.
- Know how to write their workflows as reusable shell scripts
- Understand the benefits of using version control
- Understand basic git terminology
- Have a good working knowledge of common tasks in Git
- See how Git repositories can help them to move towards practicing Open Science
No prior knowledge by the participants is necessary to participate in this course and it is intended for all scientific audiences. Participants are required to bring their own laptops to work on during the course. Network access (e.g. through Eduroam) is recommended.
Summary:
The Unix shell is a powerful tool that allows people to do complex things with just a few keystrokes. More importantly, it helps them combine existing programs in new ways and automate repetitive tasks so they aren’t typing the same things over and over again. Use of the shell is fundamental to using a wide range of other powerful tools and computing resources. The course will include hands-on live coding sessions where participants exercise the learned commands on their own computers.
Version control is the lab notebook of the digital world: it is used to keep track of what was done and to collaborate with other people. Its use is the state of the art in software development projects of all scales. However, it is not limited to software: books, papers, small data sets, and anything that changes over time or needs to be shared can and should be stored in a version control system. The course will include hands-on live coding sessions where participants exercise the learned commands on their own computers.
Learning Objectives:
After this course the participants will
- Have a fundamental understanding of how and why to use the Unix Shell
- Be comfortable with handling files and directories using the command line
- Have experience with advanced usage of the shell e.g. loops, pipes, redirects etc.
- Know how to write their workflows as reusable shell scripts
- Understand the benefits of using version control
- Understand basic git terminology
- Have a good working knowledge of common tasks in Git
- See how Git repositories can help them to move towards practicing Open Science