Time: 9:00-17:30, Saturday, January 11 2025
Venue: E10-304
9:00-9:45
Speaker: Jianlin Wang, Henan University
Title: 面向组合恒等式的定理自动生成和证明
Abstract:
自动化定理证明（ATP）传统上依赖于证明搜索，近年来，随着大语言模型的快速发展，AI赋能的定理自动证明已成为一种新范式。然而，由于现有证明数据的匮乏，基于人工智能的定理自动证明仍面临诸多挑战。针对组合恒等式定理自动证明问题，我们提出了一种结合大语言模型与强化学习的定理自动生成方法；通过融合人工形式化与定理自动生成，我们开发了一个基于Lean的组合恒等式形式化数据集LeanComb，及其相应的定理自动证明器；实验结果表明，针对组合恒等式的定理自动证明问题，我们开发的证明器在准确率上优于现有的证明器，且提出的定理自动生成方法显著提高了自动证明的效率和准确率。
10:00-11:00
Speaker: Guoxiong Gao, Peking University
Title: Applications of Large Language Models in Formal Reasoning
Abstract:
Interactive Theorem Provers (ITPs), often referred to as formal languages, offer a reliable method to eliminate errors in mathematical reasoning. Meanwhile, Large Language Models (LLMs) have shown great potential to accelerate—and even automate—the formalization process. In this talk, we will explore how LLMs are applied in key areas such as premise selection, tactic suggestion, auto-formalization, and automated theorem proving. Additionally, we will discuss how training datasets for these tasks are constructed, highlighting the impact of structural information on improving LLMs' performance in Lean-related tasks, particularly in LeanSearch and our statement formalizer.
11:15-12:15
Speaker: Huajian Xin, University of Edinburgh
Title: Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover Series
Abstract:
Recent advances in large language models have markedly influenced mathematical reasoning and automated theorem proving within artificial intelligence. Yet, despite their success in natural language tasks, these models face notable obstacles in formal theorem proving environments such as Lean and Isabelle, where exacting derivations must adhere to strict formal specifications. Even state-of-the-art models encounter difficulty generating accurate and complex formal proofs, revealing the unique blend of mathematical rigor required in this domain. In the DeepSeek-Prover series (V1 and V1.5), we have explored specialized methodologies aimed at addressing these challenges. This talk will delve into three foundational areas: the synthesis of training data through autoformalization, reinforcement learning that utilizes feedback from proof assistants, and test-time optimization using Monte Carlo tree search. I will also provide insights into current model capabilities, persistent challenges, and the future potential of large language models in automated theorem proving.
14:00-15:00
Speaker: Jiedong Jiang, Peking University
Title: Can LLM do formalization? An overview with examples
Abstract:
Recently, large language models (LLMs) have played a significant role in automated theorem proving and auto-formalization. However, the limited resources available for formal languages, combined with the inherent complexity of mathematics and coding, make this a challenging problem to solve. In this talk, we explore the details of existing automated proving systems based on Lean and analyze potential breakthrough points for enhancing their effectiveness.
15:15-16:15
Speaker: Raphael Douglas Giles, Utrecht University
Title: The importance of definitions in formalization
Abstract:
Formalization of mathematics typically involves making a lot of design decisions such as choosing which of many possible definitions will be most useful for a given formalization task and for future use by others. Seasoned formalization experts will know this well, but such choices can often be much more impactful on the difficulty of a project than any conceptual difficulties coming from the mathematical content directly. We have recently started a project on formalizing the Riemann-Roch theorem for curves, which has necessitated developing the theory of lengths of modules inside Mathlib. In doing this, we went through several different definitions of the length and various auxiliary definitions for the lemmas we needed before arriving at the final formalization. Our experience illuminates some of the practical considerations of formalisation and the importance of seemingly subtle differences in how objects are defined.
16:30-17:30
Speaker: Christian Merten, Utrecht University
Title: Formalizing the Bruhat-Tits tree in Lean
Abstract:
The Bruhat-Tits tree of SL_2 of a local field is an important tool in number theory and a very special case of a Bruhat-Tits building. In this talk, I will outline its construction in the proof assistant Lean 4 and give an application showcasing the guidance of proof assistants in proof development.
This is joint work with Judith Ludwig.
