Hausdorff Center for Mathematics Courses

HoTT in Lean4

Explore Homotopy Type Theory implementation in Lean4, focusing on advanced mathematical concepts and theorem proving techniques.

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

Automated Alignments in Mathematics

Explore automated alignments in mathematics with Thibault Gauthier, focusing on innovative techniques and applications in mathematical research and problem-solving.

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

Getting Started with Blueprint-Driven Formalization Projects in Lean

Learn to design, manage, and develop collaborative formalization projects in Lean using blueprint-driven approaches and essential tools for efficient project organization and execution.

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

Experiences from Exporting Proof Assistant Libraries

Insights into exporting libraries from proof assistants, exploring challenges and solutions for interoperability between formal systems and knowledge management.

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

Text Mining the arXiv with Large Language Models

Explore text mining techniques using Large Language Models to analyze and extract insights from the vast arXiv repository of scientific papers.

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

Building Grammar Libraries for Mathematics and Avoiding Manual Work

Explore techniques for constructing efficient grammar libraries in mathematics, focusing on automation to minimize manual effort and enhance productivity in formal language development.

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

Formalization of Nominal Equational Reasoning in PVS - Nominal Unification

Explore nominal equational reasoning and unification in PVS, focusing on formalizing techniques for handling bound variables in logical systems and programming languages.

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

Isabelle as System Platform for the Archive of Formal Proofs

Explore Isabelle's role as a system platform for the Archive of Formal Proofs, examining its impact on mathematical formalization and proof verification.

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

Big Math Libraries in Interactive Theorem Provers

Explore five key aspects of Big Math in Interactive Theorem Provers: inference, computation, concretization, narration, and organization. Learn about library sizes, searching, integration, and maintenance.

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

Translating HOL-Light Proofs to Coq

Découvrez la traduction des preuves HOL-Light vers Coq, explorant les défis et solutions pour la vérification formelle entre systèmes logiques différents.

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

Lean4Lean - Formalizing the Type Theory of Lean

Explore the formalization of Lean's type theory with Mario Carneiro, delving into advanced concepts and techniques for theorem proving and mathematical reasoning.

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

Lean4Less - A Term-Patching Framework for Eliminating Definitional Equalities in Lean

Explore a term-patching framework for eliminating definitional equalities in Lean, enhancing theorem proving efficiency and reducing computational overhead.

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

Structural Rules and Algebraic Properties of Intersection Types

Explore structural rules and algebraic properties of intersection types in lambda calculus, examining their impact on type assignment systems and programming language theory.

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

GFLean - Autoformalisation for Lean via Grammatical Framework

Explore GFLean, an innovative approach to autoformalisation in Lean using Grammatical Framework. Learn about its potential to bridge natural language and formal mathematics.

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

Formalizing Cubical Interpretations of Homotopy Type Theory

Explore cubical interpretations of homotopy type theory with Evan Cavallo, delving into formalization techniques and advanced mathematical concepts.

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