How to Solve Math Problems without Talent

Noriko Arai, National Institute of Informatics (Tokyo, Japan)
TIME: 9:15 – 10:15 July 24, 2024
LOCATION: MB 1.210

Abstract: The desire to solve mathematical problems without inherent talent has been a longstanding aspiration of humanity since ancient times. In this lecture, we delve into the complexity theory of proofs, examining the relationship between talent and the cost of proof. Additionally, we discuss the possibilities and limitations of using a fusion of computational methods, including computer algebra and natural language processing, to solve mathematical problems with machines. Join us as we explore the frontier of machine-enabled mathematical problem-solving, reflecting on its potential and boundaries in fulfilling this age-old human ambition.

Bio: Noriko Arai obtained her doctoral degree in science from the Tokyo Institute of Technology in 1997. Her research interests span various disciplines, including mathematical logic, artificial intelligence, cognitive science, math education, computer-supported collaborative learning, and the science of science policy (SoSP).
Noriko has been invited to speak at numerous international conferences and has served on program committees in these research areas. As the director of the Research Center for Community Knowledge at the National Institute of Informatics in Japan, she leads several impactful projects.
One notable project is NetCommons, a widely adopted content management system in Japanese schools. Currently, over 5,000 schools rely on NetCommons for their websites. Additionally, Noriko has directed the Researchmap Project, a platform for Japanese researchers to manage their research inputs and outputs in the field of SoSP. The platform has attracted over 0.3 million researchers, covering a substantial portion of active researchers and their work in Japan.
Another noteworthy achievement is Noriko’s leadership in the “Can an AI pass the University of Tokyo entrance exams” project, also known as the Todai Robot Project, which ran from 2011 to 2021. This project garnered significant media attention, with coverage from prominent national and international outlets, including The New York Times. Noriko’s TED talk, “Can an AI pass the University of Tokyo entrance exams?” has been translated into 23 languages and viewed by 1.7 million people.
Noriko’s recent research interest is developing a “Reading Skill Test” to assess literacy levels. The Ministry of Education and Technology recognized her contributions to academia, which awarded her the Prizes for Science and Technology in 2010 and the Commendation for Science and Technology in 2021.

Lean 4: Bridging Formal Mathematics and Software Verification

Leonardo de Moura, AWS (Seattle, US)
TIME: 11:00 – 12:00 July 25, 2024
LOCATION: MB 1.210

Abstract: This talk will explore the dual applications of Lean 4, the latest iteration of the Lean proof assistant and programming language, in advancing formal mathematics and software verification. We begin with an overview of its design and implementation.
We will detail how Lean 4 enables the formalization of complex mathematical theories and proofs, thereby enhancing collaboration and reliability in mathematical research. This endeavor is supported by a philosophy that promotes decentralized innovation, empowering a diverse community of researchers, developers, and enthusiasts to collaboratively push the boundaries of mathematical practice.
Simultaneously, we will discuss software verification applications using Lean 4 at AWS. By leveraging Lean’s dual capabilities as both a proof assistant and a functional programming language, we achieve a cohesive approach to software development and verification.
Additionally, the talk will outline future directions for Lean 4, including efforts to expand its user community, enhance user experience, and further integrate formal methods into both academic research and industrial applications.

Bio: Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.

The Art of SMT Solving

Erika Ábrahám, RWTH Aachen University (Aachen, Germany)
TIME: 11:00 – 12:00 July 27, 2024
LOCATION: MB 1.210

Abstract: SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. SMT solvers can be used as general-purpose off-the-shelf tools. Due to their impressive efficiency,  they are nowadays frequently used in a wide variety of applications.  A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem.
Besides its unquestionable practical impact, SMT solving has another great merit: it inspired truly elegant ideas, which do not only enable the construction of efficient software tools, but provide also interesting theoretical insights.
In this talk we give an introduction to the mechanisms of SAT and SMT solving, discuss some interesting ideas behind recent developments, and illustrate the usage of SMT solvers on a few application examples. 

Bio: Erika Abraham graduated in Computer Science at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the verification of concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the automated solution of arithmetic problems (SAT and SMT solvers). Since 2008 she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.