Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Impromptu Chat About Hahn-Banach Theorem in Lean

Hausdorff Center for Mathematics via YouTube

Overview

Engage in an impromptu discussion about the Hausdorff-Borel theorem (HB) in Lean with mathematician Mario Carneiro. Delve into the intricacies of formalizing this important mathematical concept within the Lean theorem prover, exploring its implementation, challenges, and implications for automated reasoning in mathematics. This 54-minute talk, presented at the Hausdorff Center for Mathematics, offers valuable insights for those interested in formal verification, theorem proving, and the intersection of mathematics and computer science.

Syllabus

Mario Carneiro: Impromptu chat about HB in Lean

Taught by

Hausdorff Center for Mathematics

Reviews

Start your review of Impromptu Chat About Hahn-Banach Theorem in Lean

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.