Morning Refreshments

9:20 - 9:30

Welcome opening remarks, Changbong Hyeon (AI center director)

9:30 - 10:30

Speaker Soonho Kong (Amazon Web Services) 

Title Lean into the Future -- New Horizons in Mathematics, Programming, and AI

Abstract The formal verification system Lean represents a remarkable convergence of mathematical logic, computer science, and artificial intelligence. This talk explores how Lean is transforming the way we think about mathematical proof, software correctness, and reasoning. At its core, Lean provides a precise language for expressing mathematical statements and proofs in a way that can be verified by computer. But it is much more than just a proof checker: it serves as a platform for collaborative mathematics, a framework for verified software development, and an experimental ground for AI-assisted theorem proving.

The presentation will demonstrate how the mathematical community is using Lean to formalize complex mathematical proofs, enabling unprecedented levels of collaboration and verification. In software development, examples will show how Lean's dependent type theory allows developers to write provably correct programs and implement aggressive optimizations with confidence. The discussion will conclude with exciting developments at the intersection of Lean and AI, including development of AI-powered proof automation. Throughout, these developments illustrate how Lean addresses long-standing challenges in mathematics, software reliability, and AI trustworthiness.

11:00 - 12:00

Speaker Byung-Hak Hwang (KIAS) 

Title Formalizing mathematics: why and how

Abstract Formalizing mathematics involves translating mathematical statements from natural language into a precise formal language that computers can understand. As modern mathematics becomes deeper and more complex, the importance of formalization has grown significantly. In this talk, I will introduce the concept of formalization, explore its significance, and highlight current successful and ongoing projects in the field.

Lunch

1:30 - 2:30

Speaker Yeachan Park (KIAS) 

Title Autoformalization and Automated Theorem Proving with Language Models

Abstract In this talk, we will discuss autoformalization and automated theorem proving. Autoformalization refers to the task of automatically translating natural language into a formal language. While using proof assistants to verify proofs is effective, it requires users to write proofs in formal language, which can be challenging and time-consuming even for mathematicians, creating a significant barrier to entry. We introduce recent advances in autoformalization using language models. Although the current quality of translation is far from perfect and often fails with complex statements, fine-tuning large language models shows promising results in autoformalization.

We will also discuss automated theorem proving (ATP), which generates proofs for theorems in formal language. Our focus is on ATP using language models, opening new pathways for theorem proving. Recent progress in ATP is driven by the availability of extensive mathematical data and advanced Lean tactics. Through the integration of machine learning and proof assistants, ATP has successfully solved high-school-level Olympiad math problems. However, solving college-level math problems remains a challenge for ATP. We will explore the current status and future directions of ATP.

3:00 - 4:00

Speaker Jineon Baek (Yonsei University) 

Title Getting Started with Lean 4: A Hands-On Tutorial for Mathematicians

Abstract This tutorial introduces Lean 4, a tool for formalizing and verifying mathematical proofs. The session is designed for mathematicians, including professors, graduate students, and postdocs, with no prior experience required. We will work through simple examples together, with live demonstrations that you can (and are encouraged) follow on your own laptop. Questions are encouraged throughout the session to make it interactive and helpful.

4:30 - 5:30

Tutorial on Lean

Please bring your own laptop.

Zulip invitation:  https://lean-in-korea.zulipchat.com/join/blti3xozhbek6opyylpuu6kb/

Dinner