University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Smooth vector bundles in Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Smooth vector bundles in Lean

Download to your calendar using vCal

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki .

Hybrid talk (please see abstract for link)

Abstract: I will report on the formalization of the definition of a smooth vector bundle in Lean. A number of subtleties arise here, and I will make the case that these are subtleties not just of formalization but of mathematics. This is joint work with Floris van Doorn.

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 379 992 884 209 Passcode: TYR8 Sh

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Centre for Mathematical Sciences, MR14/Talk Cancelled israel Clare Hall Lecture: The evolution of Abcam plc - 30 April 2013

Other talks

Title to be confirmed The Play Paradox: How video games build better humans Title to be confirmed Secrets of the Surface: The Mathematical Vision of Maryam Mirzakhani ( EDI Film Screening) Market Failure, Organ Shortage, Pandemic and Climate Change: The Architecture of Cooperation Sera Markoff Inaugural Lecture for the Plumian Professorship in Astronomy and Experimental Philosophy - 'Staring into the heart of darkness: from theory to the direct imaging of black holes'
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity