• Start Date: March 29, 2023
  • Event Start Time: 12:30 PM
  • Event End Time: 2:00 PM
  • Seminar Series: Rutgers LEAN (Mathematics) Seminar
  • Presenter(s): Andre Hernandez-Espiet - Rutgers University
  • Event Location: Hill Center, Room 005
  • Presentation Type: Stand Alone Presentation
  • Abstract:

    "Mathlib" or the library of mathematical proofs written in Lean was developed using a version of Lean called Lean 3. A new version of Lean, Lean 4, which addresses many shortcomings of Lean 3, was recently released. In this talk, we will discuss the differences between Lean 3 and Lean 4, installing Lean 4, and potentially porting over previous code written by seminar participants to Lean 4.