BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A formalisation of a special case of the Union-Closed Conjecture a
 nd formal proofs as datasets in the era of LLMs - Angeliki Koutsoukou-Argy
 raki (Royal Holloway\, University of London)
DTSTART:20250612T081500Z
DTEND:20250612T091500Z
UID:TALK230638@talks.cam.ac.uk
DESCRIPTION:I will discuss a formalisation in Isabelle/HOL of a proof of a
  special case of the Union-Closed Conjecture by J. Aaronson\, D. Ellis and
  I. Leader showing that the Union-Closed Conjecture holds for the union-cl
 osed family generated by the cyclic translates of any fixed set (joint wor
 k with L. C. Paulson). I will then use our formalisation as an example to 
 motivate a discussion raising the question of exploring what design choice
 s to make while developing formal proofs when viewing them as potentially 
 useful datasets for LLMs.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR