• Start Date: April 5, 2023
  • Event Start Time: 12:30 PM
  • Event End Time: 2:00 PM
  • Seminar Series: Rutgers LEAN (Mathematics) Seminar
  • Presenter(s): Alex Kontorovich - Rutgers University
  • Event Location: Hill Center, Room 005
  • Presentation Type: Stand Alone Presentation
  • Abstract:

    In this talk, we will discuss the differences between using Lean 3 and Lean 4 to write Euclidean geometry proofs. We will also discuss how to define convex polygons in Lean in order to simplify proofs involving areas.