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:In this second talk, we will provide an overview of the design and implemen
 tation of the metaprogramming capabilities in Sequencelib, including the OE
 IS attribute, which can be used to automatically attach OEIS sequence metad
 ata to a Lean definition, and the oeis-tactic, which can be used to automat
 ically prove theorems about the values of sequences. We also detail OEIS-LT
 , a lightweight, multi-threaded Lean tool server that bundles these capabil
 ities into a scalable, machine-friendly API. Together, these tools support 
 automated formalization and proof synthesis (AFPS) workflows, and as an exa
 mple, we describe the design and implementation of a computational pipeline
  that built on the work of Gauthier, et al. and leveraged OEIS-LT to formal
 ize more than 25,000 sequences from the OEIS. Finally, we describe how OEIS
 -LT will be included in a new AFPS toolchain we have started building with 
 our collaborators called AIProver, and we present some preliminary results 
 from its initial use on Sequencelib. \n
X-ALT-DESC;FMTTYPE=text/html:<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:20260826T094805
DTSTART;TZID=America/New_York:20260416T110000
DTEND;TZID=America/New_York:20260416T120000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR