Seminar Details
Euclidean Geometry in Lean 4
- 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.
