Hausdorff Center for Mathematics Courses

Condensed Mathematics in Mathlib

Explore condensed mathematics in Mathlib with Dagur Asgeirsson, delving into advanced mathematical concepts and their implementation in the Lean theorem prover's mathematics library.

• YouTube
• 59 minutes
• Self-Paced
• Free Video

A Taste of ELPI - Introduction to Extensible Logic Programming Interpreter

Explore ELPI, a programming language for implementing type-checkers and elaborators. Learn its features, applications, and potential in theorem proving and meta-programming.

• YouTube
• 36 minutes
• Self-Paced
• Free Video

Extending the Lean User Interface with Widgets - A Tutorial

Learn to create interactive visualizations and widgets for the Lean 4 proof assistant, enhancing mathematical communication and exploration of formal proofs and computations.

• YouTube
• 32 minutes
• Self-Paced
• Free Video

Beautiful Formalizations and Proofs in Mechanized Mathematics

Explore the aesthetics of mathematical formalization, examining how beauty in mathematics adapts to mechanization and automation, with illustrative examples of elegant definitions and proofs.

• YouTube
• 40 minutes
• Self-Paced
• Free Video

From Informal to Formal Mathematics and Back - Tools for Mathematical Transformation

Tools for transforming informal mathematics to formal and vice versa, aiming to enhance mathematical understanding. Explores Lean blueprint infrastructure and Informal Lean for collaborative formalization projects and customizable proof detailing.

• YouTube
• 42 minutes
• Self-Paced
• Free Video

Lean-HoG: Incorporating a Database of Graphs into a Proof Assistant

Explore the integration of a graph database into a proof assistant, enhancing mathematical reasoning capabilities and streamlining complex proofs in formal verification.

• YouTube
• 36 minutes
• Self-Paced
• Free Video

Formalising the Theory of Combinatorial Optimisation

Explore formalisation of combinatorial optimisation theory in Isabelle/HOL, focusing on matching theory and its mathematical implications for computer science and applied mathematics.

• YouTube
• 35 minutes
• Self-Paced
• Free Video

Unavoidable Mathematics - Exploring Derived Concepts from Simple Theories

Exploring fundamental mathematical concepts that arise naturally from simple theories, revealing unexpected connections and rich structures in algebra, category theory, and computer science.

• YouTube
• 34 minutes
• Self-Paced
• Free Video

Inverse Results for Isoperimetric Inequalities - Lecture 4

Explore inverse isoperimetric problems in graphs, focusing on the Fourier-Entropy-Influence conjecture and related inequalities. Progress and applications in PAC learning discussed.

• YouTube
• 1 hour 19 minutes
• Self-Paced
• Free Video

Inverse Results for Isoperimetric Inequalities - Lecture 3

Explore inverse isoperimetric problems in graphs, focusing on the Fourier-Entropy-Influence conjecture and related inequalities. Progress and applications discussed.

• YouTube
• 1 hour 11 minutes
• Self-Paced
• Free Video

Multiscale Approximations for the Stationary Ginzburg-Landau Equation

Explores discrete minimizers of Ginzburg-Landau energy in finite element spaces, focusing on parameter κ's influence on vortex lattices and mesh resolution conditions for accurate numerical simulations.

• YouTube
• 44 minutes
• Self-Paced
• Free Video

Dynamic Brittle Fracture as a Well-Posed Nonlocal Initial Value Problem

Explore a nonlocal model for dynamic brittle damage, examining its phases, evolution, and energy balance. Learn how this approach relates to Griffith fracture energy and Navier's equation for crack propagation.

• YouTube
• 50 minutes
• Self-Paced
• Free Video

Asymptotics of Optimal Constants in the Khinchine-Kahane Inequality

Explore the asymptotics of optimal constants in Khinchine-Kahane inequality, examining classical moment inequalities for Rademacher sums and recent developments in this century-old field of study.

• YouTube
• 1 hour 22 minutes
• Self-Paced
• Free Video

Inverse Results for Isoperimetric Inequalities - Part II

Explores inverse isoperimetric problems in graphs, focusing on the Fourier-Entropy-Influence conjecture and related inequalities, with applications to PAC learning and other areas.

• YouTube
• 1 hour 14 minutes
• Self-Paced
• Free Video

Sharp Fourier Restriction Theory Over Finite Fields

Explore recent developments in sharp Fourier restriction theory over finite fields, examining the intersection of two key areas in mathematical research.

• YouTube
• 52 minutes
• Self-Paced
• Free Video