Seminar Details
Formalizing a Second Proof of the Pythagorean Theorem
- Start Date: March 8, 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
- Event Additional Info: <p>A Zoom option to attend is available. Please contact one of the organizers for the link.</p>
- Presentation Type: Stand Alone Presentation
- Abstract:
Over the past few weeks, seminar participants have been working on formalizing a second proof of the Pythagorean theorem in Lean. In this talk, we will give an introduction to the framework used for doing Euclid’s Elements in Lean. Various participants will then share their recent progress on the second proof. This talk will not assume prior experience with Lean and will aim to be accessible to people not already engaged in the Pythagorean theorem project.