BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Lean Tactic to Automatically Generalize Proofs - Anshula Gandhi 
 (University of Cambridge)
DTSTART:20251030T170000Z
DTEND:20251030T180000Z
UID:TALK238816@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:We present an algorithm\, developed in the Lean programming la
 nguage\, to automatically generalize mathematical proofs.  The algorithm\,
  which builds on work by Olivier Pons\, advances state-of-the-art proof ge
 neralization by robustly generalizing repeated and related constants\, as 
 well as abstracting out hypotheses implicitly concerning them.\nFor exampl
 e\, consider the theorem that sqrt(2)  is irrational. This algorithm exami
 nes the statement and its proof\, and by checking which lemmas in the proo
 f are used\, determines that the only property of 2 used in the proof is t
 hat it is prime. So\, the algorithm produces a more general statement: tha
 t sqrt(p) is irrational\, where p is any prime.\nNote\, however\, that the
  algorithm does not derive the more generally true theorem — that the sq
 uare root of any number that is not a perfect square is irrational — whe
 n that reasoning step is not evident in the proof term. Roughly speaking\,
  the algorithm generalizes the theorem only as far as the proof allows. We
  refer to this type of generalization as proof-based generalization.\n\n==
 = Hybrid talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/8985609
 1954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Pas
 scode: ITPtalk
LOCATION:Centre for Mathematical Sciences\, MR14
END:VEVENT
END:VCALENDAR