Lean for the curious mathematician / Lean pour mathématiciens

Collection Lean for the curious mathematician / Lean pour mathématiciens

Organizer(s) Brasca, Riccardo ; Chambert-Loir, Antoine ; de Frutos-Fernández, María Inés ; Nuccio , Filippo

Date(s) 25/03/2024 - 29/03/2024

linked URL https://conferences.cirm-math.fr/2970.html

00:00:00 / 00:00:00

3 4

Complex analysis in Lean

By Vincent Beffara

I present a formalization of the Riemann Mapping Theorem in the Lean 4 proof assistant, and a few related topics.

Information about the video

Date of recording 26/03/2024
Date of publication 22/04/2024
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Luca Recanzone
Format MP4

Citation data

DOI 10.24350/CIRM.V.20153203
Cite this video Beffara, Vincent (26/03/2024). Complex analysis in Lean. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20153203
URL https://dx.doi.org/10.24350/CIRM.V.20153203

Domain(s)

Logic in Computer Science

MSC codes

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

All the collection videos

01:03:23

published on April 22, 2024

Stone duality and its formalization

By Sam van Gool

01:01:09

published on April 22, 2024

Working with Mathlib

By Jireh Loreaux

48:48

published on April 22, 2024

Complex analysis in Lean

By Vincent Beffara

01:34:11

published on April 22, 2024

Coq/Rocq tutorial: Ssreflect tactics and the MathComp library

By Marie Kerjean

Copyright Carmin.tv 2024

Give feedback