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:20250407T100000
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:ac3ba4fe17df583388df008b7cdb4ddc
CATEGORIES:Lean Seminar
CREATED:20260407T123809
SUMMARY:Searching for (formal) proofs
LOCATION:Hill 705
DESCRIPTION:In 2025, Harmonic, along with three other companies, achieved a gold medal-
 level performance at the IMO with AI systems, a feat that could only have b
 een described as science fiction not many years ago. In this talk, I will p
 resent Aristotle, our reinforcement learning system that achieved this feat
 , discussing both its Monte Carlo tree search-based Lean proof search, and 
 the frameworks we used to augment its capabilities - test-time training, an
 d lemma generation. I will then highlight some work done by newer versions 
 of Aristotle, autonomously solving problems without human input, and assist
 ing mathematicians with large-scale formalizations.\n
X-ALT-DESC;FMTTYPE=text/html:<p><span data-olk-copy-source="MessageBody" style="font-size: 13px; font-fa
 mily: 'Helvetica Neue'; margin: 0px; line-height: normal;">In 2025, Harmoni
 c, along with three other companies, achieved a gold medal-level performanc
 e at the IMO with AI systems, a feat that could only have been described as
  science fiction not many years ago. In this talk, I will present Aristotle
 , our reinforcement learning system that achieved this feat, discussing bot
 h its Monte Carlo tree search-based Lean proof search, and the frameworks w
 e used to augment its capabilities - test-time training, and lemma generati
 on. I will then highlight some work done by newer versions of Aristotle, au
 tonomously solving problems without human input, and assisting mathematicia
 ns with large-scale formalizations.</span></p>
CONTACT:Eric Rodriguez (Harmonic)
DTSTAMP:20260826T234344
DTSTART;TZID=America/New_York:20260408T100000
DTEND;TZID=America/New_York:20260408T110000
SEQUENCE:0
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR