BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Human oriented tools for theorem proving in Lean - Jovan Gerbsheid
  (University of Cambridge)
DTSTART:20251120T170000Z
DTEND:20251120T180000Z
UID:TALK240100@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:I will present some tactics and tools that I made for Mathlib.
  I will explain how they work and show them in action with a live demonstr
 ation. The main ones are\n\n- A library search tool for finding theorems b
 ased on an expression in the tactic state\n\n- The generalized rewriting t
 actic for rewriting with relations other than equalitys.\n\n=== Hybrid tal
 k ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba
 77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Passcode: ITPta
 lk\n
LOCATION:Centre for Mathematical Sciences\, MR14
END:VEVENT
END:VCALENDAR