BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//jEvents 2.0 for Joomla//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:STANDARD
DTSTART:20251102T010000
RDATE:20260308T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20261101T010000
RDATE:20270314T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20271107T010000
RDATE:20280312T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:STANDARD
DTSTART:20281105T010000
RDATE:20290311T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20250415T110000
RDATE:20251102T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20260308T030000
RDATE:20261101T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20270314T030000
RDATE:20271107T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
BEGIN:DAYLIGHT
DTSTART:20280312T030000
RDATE:20281105T010000
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:America/New_York EDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:42940c0890ebe4dfb7a659d10d4f72f8
CATEGORIES:Lean Seminar
CREATED:20260411T101900
SUMMARY:Automated Formalization of OEIS using the Sequencelib Platform
LOCATION:Hill 005
DESCRIPTION:<p><span data-olk-copy-source="MessageBody" style="text-align: left; text-i
 ndent: 0px; background-color: #ffffff; margin: 0px; font-family: Aptos, Apt
 os_EmbeddedFont, Aptos_MSFontService, Calibri, Helvetica, sans-serif; font-
 size: 12pt; color: black;">In this second talk, we will provide an overview
  of the design and implementation of the metaprogramming capabilities in Se
 quencelib, including the OEIS attribute, which can be used to automatically
  attach OEIS sequence metadata to a Lean definition, and the oeis-tactic, w
 hich can be used to automatically prove theorems about the values of sequen
 ces. We also detail OEIS-LT, a lightweight, multi-threaded Lean tool server
  that bundles these capabilities into a scalable, machine-friendly API. Tog
 ether, these tools support automated formalization and proof synthesis (AFP
 S) workflows, and as an example, we describe the design and implementation 
 of a computational pipeline that built on the work of Gauthier, et al. and 
 leveraged OEIS-LT to formalize more than 25,000 sequences from the OEIS. Fi
 nally, we describe how OEIS-LT will be included in a new AFPS toolchain we 
 have started building with our collaborators called AIProver, and we presen
 t some preliminary results from its initial use on Sequencelib.&nbsp;</span
 ></p>
CONTACT:Joe Stubbs
DTSTAMP:20260826T094726
DTSTART;TZID=America/New_York:20260416T110000
DTEND;TZID=America/New_York:20260416T120000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR