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

YouTube

Formal Mathematics for Mathematicians and Mathematics Students - IPAM at UCLA

Institute for Pure & Applied Mathematics (IPAM) via YouTube

Overview

Explore the potential impact of formal mathematics on mathematical exposition in this 55-minute conference talk by Patrick Massot from Université Paris-Saclay. Delve into how formal methods can benefit mathematicians beyond proof verification, with a focus on their application in teaching and communicating mathematical concepts. Witness a demonstration of readable proof scripts, English translations, and the use of AI tools in formalizing mathematical proofs. Gain insights into topics such as general topology, proof structure, and the future of formal mathematics in academic settings. Discover practical examples using Lean, a theorem prover and programming language, and learn how it can be applied to complex mathematical concepts like open sets, neighborhoods, and subsets.

Syllabus

Intro
Topology
General topology
Proof structure
Formalization
readable proof script
English translation
Open AI DaVinci
Tiny URL
Gold State
Close Neighborhood
Set Image Subset
Lean Informal
Future steps
Complicated proof
Unreliable proof
Technical talk
Lean code
Simp
Proof in Lean
Python
Lean

Taught by

Institute for Pure & Applied Mathematics (IPAM)

Reviews

Start your review of Formal Mathematics for Mathematicians and Mathematics Students - IPAM at UCLA

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.