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:20241104T133000
RDATE:20250309T030000
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:America/New_York EST
END:STANDARD
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:20250309T030000
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:2645e4d666bf227de6b962a4e883293a
CATEGORIES:Lean Seminar
CREATED:20251025T133202
SUMMARY:O-Forge: a verifiable, LLM-driven framework for proving inequalities in research mathematics.
LOCATION:CoRE 431
DESCRIPTION:<p><span style="font-style: normal; font-weight: 400; letter-spacing: norma
 l; text-indent: 0px; text-transform: none; white-space: normal; word-spacin
 g: 0px; text-decoration: none; color: #555555; font-family: 'Open Sans', sa
 ns-serif; font-size: 18px; orphans: 2; text-align: left; widows: 2; backgro
 und-color: #ffffff; float: none;">We introduce an LLM + computer software f
 ramework for proving sophisticated inequalities in research mathematics. We
  first ask a frontier LLM to break up a problem into its simplest parts, an
 d then ask a computer algebra system to complete the proof for each part. I
 n doing so, we resolve a problem posed by Terence Tao about AI for Mathemat
 ics. This is joint work with Vijay Ganesh (Georgia Tech).</span></p>
CONTACT:Ayush Khaitan
DTSTAMP:20260922T065540
DTSTART;TZID=America/New_York:20251105T133000
DTEND;TZID=America/New_York:20251105T150000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR