BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
PRODID:adamgibbons/ics
METHOD:PUBLISH
X-PUBLISHED-TTL:PT1H
BEGIN:VEVENT
UID:qDNBuLPwPpgFiaZRwiJkv
SUMMARY:Autoformalization for the Working Mathematician
DTSTAMP:20260330T195000Z
DTSTART;VALUE=DATE:20250424
DTEND;VALUE=DATE:20250427
DESCRIPTION:A large community of pure mathematicians has recognized the imp
	ortance of formal verification in modern mathematics and is looking forwar
	d to systems like Lean becoming an everyday tool in research. At the same 
	time\, automated theorem proving has recently become popular in the machin
	e learning community as a benchmark and stepping stone for the more genera
	l task of automated reasoning. The goal of this workshop is to bring these
	 communities together.\n\nWe will have talks and tutorials that introduce 
	mathematicians to Lean and to state-of-the-art technologies in automated t
	heorem proving. We will also discuss future research directions\, tooling\
	, and other ways to make this technology more useful to working mathematic
	ians. Our medium-term goal is to initiate an effort in the mathematical co
	mmunity to develop a well-aligned dataset that can be used to benchmark mo
	dels for tasks that are close to the use cases of working mathematicians. 
	The first afternoon of the workshop will be a hackathon whose goal is to c
	reate tools that will aid mathematicians in this dataset creation.
URL:https://icerm.brown.edu/program/hot_topics_workshop/htw-25-aftwm
LOCATION:Institute for Computational and Experimental Research in Mathemati
	cs\, Brown University
END:VEVENT
END:VCALENDAR