The tutorial is designed for a broad audience across natural language processing, machine learning, formal methods, theorem proving, mathematical reasoning, and AI for science.
No. Prior experience with formal languages, theorem provers, or formal mathematics is not required.
The tutorial introduces the key concepts before moving to more advanced topics.
A general understanding of mathematics at the high-school or undergraduate level is sufficient.
Some undergraduate-level mathematical maturity may be helpful for examples involving formal mathematics and scientific applications.
A basic understanding of large language models is helpful, particularly concepts such as prompting and AI agents.
The tutorial introduces both Isabelle and Lean4.
Yes. The tutorial emphasizes intuitive explanations, qualitative demonstrations, and practical examples.
Topics include few-shot and retrieval-augmented autoformalization, refinement using feedback, and evaluation of generated formalizations.
Yes. The tutorial includes examples from physics and discusses how autoformalization may support more rigorous and verifiable scientific reasoning.
The primary focus is autoformalization: translating informal mathematical statements into formal representations.
This differs from theorem-proving tutorials that start from statements that have already been formalized.
Participants should gain an understanding of the main components of an autoformalization pipeline, including formalization, retrieval, refinement, and evaluation, as well as current challenges and opportunities for future research.