Working with Mathlib - Lecture 1

Explore a comprehensive conference talk on working with Mathlib, presented by Jireh Loreaux at the Centre International de Rencontres Mathématiques in Marseille, France. Recorded during the thematic meeting "LEAN pour mathématiciens" on March 26, 2024, this hour-long presentation delves into the intricacies of utilizing Mathlib in mathematical research and applications. Gain valuable insights into leveraging this powerful library for advanced mathematical computations and proofs. Access this video and other talks by renowned mathematicians through CIRM's Audiovisual Mathematics Library, featuring chapter markers, keywords, enriched content with abstracts and bibliographies, and a multi-criteria search function for easy navigation through mathematical topics and areas of interest.