• Start Date: May 4, 2023
  • Event Start Time: 1:30 PM
  • Event End Time: 2:30 PM
  • Seminar Series: Rutgers LEAN (Mathematics) Seminar
  • Presenter(s): Heather Macbeth - Fordham University
  • Event Location: Hill Center, Room 701
  • Presentation Type: Stand Alone Presentation
  • 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.