• Start Date: May 3, 2023
  • Event Start Time: 10:00 AM
  • Event End Time: 11:00 AM
  • Seminar Series: Rutgers LEAN (Mathematics) Seminar
  • Presenter(s): Heather Macbeth - Fordham University
  • Event Location: Hill Center- Room 525 | Rutgers University
  • Presentation Type: Stand Alone Presentation
  • Abstract:

    I will report on my experience teaching with Lean in an early-undergraduate (1st and 2nd year students) mathematics course: an intro-to-proof course with an emphasis on concrete numeric examples.  The course is genuinely bilingual between English and Lean, with every proof carried out in parallel formally and informally.  Substantial custom automation supports proof-writing at the same level of detail as is required of the students on paper, notably in calculational proofs of equalities, inequalities and (modular-arithmetic) congruences.