Speaker Introduction

Mr. Wang Yutong is currently a master student at the National University of Singapore. He got his Bachelor of Science from Soochow University.

Abstract

The growing of verifiable formal languages, particularly interactive proof assistants like Lean 4, is shaping the future of mathematics and transforming how large language models (LLMs) can assist in automated reasoning. However, navigating the vast and complex Mathlib and composing reliable formal statements remains a challenge, with arcane syntax and scattered lemmas. In this talk, I will present our recent developments: the Lean Search platform V2and the Herald translator, which features Lean-aware LLMs to streamline proof writing and auto-formalization of statements. We will explore specialized model training and data augmentation techniques that enhance LLM-accelerated formalization. I will demonstrate how these tools can assist both mathematicians and Lean developers. Topic: AI4M Series: Accelerating Formalization with Lean and LLMs Time: Oct 17, 2024 03:30 PM Singapore, Join Zoom Meeting.https://nus-sg.zoom.us/j/81155995432?pwd=dklGWQbkQ9sWzIJKVpJ2FpmRp4q3bx… ID: 811 5599 5432Passcode: 084713