Workshop on Artificial Intelligence for Mathematics (AI4Math)

Program and Informal, Non-Archival Proceedings

Time	Talk (Speaker)
9:00 - 10:00	A Decade of ATP Tuning: Machine Learning, Strategy Invention, and AI in the Future (Jan Jakubův, Invited Speaker)
10:00 - 10:30	Coffee Break
10:30 - 10:50	Flexiformality and LLM-Assisted Mathematics (Dennis M. Müller)
10:50 - 11:10	Semantic Representation and Computation for Pure Mathematics in the Wolfram Language (Ian Ford)
11:10 - 11:30	PIDE MCP: Connecting AI Agents to Isabelle (Kevin Kappelmann)
11:30 - 11:50	10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean (Vaibhav Bajpai, Nathan Bowler, Johannes Carmesin, Utku Okur)
11:50 - 12:10	AutoGraphForge: Conjecturing, Refutation and Lean Proving in One Loop (Ján Pastorek)
12:10 - 12:30	Closing Remarks

Last modified: September 25 2026 12:42:38 CEST