BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Towards the Automatic Mathematician: The Past\, The Present\, and 
 the Next Few Months Ahead (Yes\, Really) [Oberseminar Discrete Optimizatio
 n]
DTSTART:20260521T161500Z
DTEND:20260521T171500Z
DTSTAMP:20260518T072100Z
UID:indico-event-1289@math-events.uni-bonn.de
DESCRIPTION:Speakers: Christian Szegedy (AletheAI)\n\n \nAutoformalizatio
 n\, the automatic translation of informal mathematics into machine-verifia
 ble formal statements and proofs\, has been the unifying theme of my resea
 rch since founding the N2Formal team in 2016 at Google ("into-formal" or "
 N²-formal\," where N² nods to neural networks).\nOur first major result\
 , DeepMath\, showed that deep sequence models could effectively guide prem
 ise selection in large formal libraries. This laid the foundation for co-t
 raining theorem proving and autoformalization. The vision continued throug
 h tactic prediction for higher-order logic\, reasoning in latent space\, a
 nd early LLM-based autoformalization. That work demonstrated that transfor
 mers could already translate non-trivial portions of competition-level mat
 hematics into Isabelle/HOL.\nToday\, systems like the Gauss agent (Math\, 
 Inc.) are semi-autonomously formalizing advanced results\, such as the str
 ong version of the Prime Number Theorem in Lean. It generated tens of thou
 sands of verified lines in roughly three weeks\, work that would likely ta
 ke a human team many months.\nThe progress is accelerating. In the next fe
 w months\, the focus will shift from single-agent systems to multi-agent e
 cosystems where specialized AI agents collaborate\, compete\, and improve 
 via carefully designed market mechanisms. Agents will trade conjectures\, 
 proofs\, and predictions in a shared database\, creating open-ended\, ince
 ntive-aligned collective intelligence while building a vast repository of 
 fully formalized and verified mathematics\, and learning super-human reaso
 ning skills along the way.\n \n \nThis Oberseminar takes place in the Ge
 rhard-Konow-Hörsaal\, Lennéstr. 2. Participants are invited to have cof
 fee or tea in the lounge\, 2nd floor\, before.\n \n\nhttps://math-events.
 uni-bonn.de/event/1289/
LOCATION:Arithmeum\, Lennéstr.\,  2 - Gerhard Konow-Hörsaal (Arithmeum /
  Research Institute for Discrete Mathematics)
URL:https://math-events.uni-bonn.de/event/1289/
END:VEVENT
END:VCALENDAR