Description

    The intersection of Artificial Intelligence (AI) and mathematics has led to groundbreaking advancements, particularly in the domain of formal theorem proving. AI's ability to enhance and automate reasoning processes is transforming the way mathematical proofs are developed, verified, and understood. Central to this revolution is the Lean theorem prover, a powerful tool that is increasingly being adopted for formalizing complex mathematical theorems and facilitating rigorous proof verification.

    From September 2nd to 4th, Peking University will host the "AI for Mathematics Workshop on Lean, Automated Reasoning, and Beyond," a conference dedicated to the forefront of AI-driven formalization in mathematics, with a special focus on Lean. This event will bring together leading experts, researchers, and practitioners who are pioneering the use of Lean for formal theorem proving and use AI models as assisting tools. The conference will feature a series of talks and presentations that delve into the latest developments in Lean, its applications in mathematical research, and its role in the broader landscape of AI and automated reasoning.

    Following the main conference, from September 5th to 6th, an intensive Lean workshop will be held, offering hands-on experience in using Lean for formal verification and theorem proving. This workshop is designed to equip participants with practical skills and a deep understanding of Lean’s potential to formalize and automate theorems, making it an invaluable resource for researchers and practitioners alike.

    Whether you are an AI researcher, a mathematician, or a practitioner in automated reasoning systems, this conference offers a unique opportunity to immerse yourself in the world of formalized mathematics with Lean, and to contribute to the discussions that are defining the future of this exciting field.

Conference Schedule

Poster