Hausdorff Center for Mathematics Courses

Theory-Oriented Mathematics in Modern Research

Explore theory-oriented mathematics with Juan Meleiro in this insightful seminar, delving into advanced concepts and their applications in modern mathematical research.

• YouTube
• 54 minutes
• On-Demand
• Free Video

Categories, Axioms, and Constructions in SageMath - Modeling Mathematics for Fun and Profit

Explore mathematical modeling using SageMath, focusing on categories, axioms, and constructions. Learn to apply these concepts for both enjoyment and practical applications.

• YouTube
• 1 hour 2 minutes
• On-Demand
• Free Video

Linear Algebra Game in Lean

Explore linear algebra concepts through interactive gameplay in Lean, enhancing mathematical understanding and problem-solving skills.

• YouTube
• 50 minutes
• On-Demand
• Free Video

Building Measure Theory Using Hierarchy Builder

Explore the Hierarchy Builder DSL for Coq and its application in constructing measure theory and Lebesgue measure, with insights for potential adaptations to other proof assistants.

• YouTube
• 40 minutes
• On-Demand
• Free Video

Towards a Formalized Proof of Carleson's Theorem

Explores formalizing Carleson's theorem on Fourier series convergence, discussing its significance, challenges, and recent generalizations in metric spaces using the Lean theorem prover.

• YouTube
• 39 minutes
• On-Demand
• Free Video

Formalising Advanced Mathematics in Isabelle/HOL

Explore the formalisation of advanced mathematics using Isabelle/HOL, discussing accomplishments and conclusions from a six-year research project and its unique considerations.

• YouTube
• 34 minutes
• On-Demand
• Free Video

HOL with Dependent Types and Subtyping

Explore advanced type theory concepts combining Higher-Order Logic, dependent types, and subtyping for enhanced formal reasoning and theorem proving capabilities.

• YouTube
• 33 minutes
• On-Demand
• Free Video

Programming Mathematics - Tools and Challenges

Explore tools and challenges in programming mathematics with Georges Gonthier, delving into innovative approaches for formalizing complex mathematical concepts.

• YouTube
• 43 minutes
• On-Demand
• Free Video

Verifying Elliptic Curve Computations on Blockchain

Explore the intersection of blockchain technology and elliptic curve cryptography, focusing on verification methods for secure and efficient computations in decentralized systems.

• YouTube
• 38 minutes
• On-Demand
• Free Video

Formalisation and Automation of Foundational Theories - A LogiKEy Perspective

Explores formalizing theories beyond mathematics, emphasizing legal and ethical domains for AI control. Discusses intelligent cut-introduction in proof automation and advocates for increased focus on free logic and counter-model finding.

• YouTube
• 42 minutes
• On-Demand
• Free Video

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
• On-Demand
• 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
• On-Demand
• 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
• On-Demand
• 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
• On-Demand
• 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
• On-Demand
• Free Video