AI for Formal Math

This direction focuses on automated theorem proving, autoformalization, and the intersection of large language model mathematical reasoning with formal verification, with emphasis on the Lean 4 ecosystem, including proof search, premise selection, translation from natural-language mathematics to formal language, and mathematical library development. It aims to advance formal solutions to IMO/Putnam-level problems, while valuing reproducible artifacts (code, benchmarks, Lean libraries) and community dynamics (e.g., Lean Zulip, Mathlib progress) alongside research papers.