• Start Date: March 22, 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:

    This week the Lean group will discuss the uniformization of the code for the second proof of the Pythagorean theorem. This includes naming conventions for theorems and variables, creating a cataloguing system for said theorems, discussion about snippets in VSCode, making the code more efficient through the use of different tactics, and general code maintenance and documentation conventions.