dimacs logo color

Events

Event Calendar

« Previous Month

August 2026

Next Month »
Sun Mon Tue Wed Thu Fri Sat
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

Seminar Details

Metaprogramming for Mathematics

  • Start Date: May 4, 2023
  • Event Start Time: 10:00 AM
  • Event End Time: 11:00 AM
  • Seminar Series: Rutgers LEAN (Mathematics) Seminar
  • Presenter(s): Robert Lewis - Brown University
  • Event Location: Hill Center, Room 701
  • Presentation Type: Stand Alone Presentation
  • Abstract:

    The Lean 3 metaprogramming framework is designed to allow users to extend the tactic (proof) language in various ways. I'll go over some details about the distinction between the object and meta language of Lean, looking foundationally at how tactics work. I'll describe some extensions that have been added to the Lean 3 mathlib library to help build a more natural mathematical vernacular in the proof language.