연사: Dr. Soonho Kong (Amazon Web Services), developer of the programming language Lean

 

장소:  27동 220호

시간: 12월 19일 목요일 11시

 

제목:  Lean into the Future -- New Horizons in Mathematics, Programming, and AI

초록: 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.