报告题目：Cosmology in the Age of AI and Formalization

报告人：李金政 博士（IBS-CTPU-PTC）

报告时间：2026 年 10 月 8 日（周四）15 : 30-16 : 30

报告地点：北洋园校区 49 教 410 室

报告摘要：

AI offers new ways to explore cosmological models and develop theoretical arguments, yet convincing derivations can conceal subtle errors with serious consequences. This talk introduces mathematical formalization as a way to make assumptions explicit and produce computer-checked proofs. Using Lean, we explain how proof assistants work, why they complement tools such as Mathematica, and how AI can both assist proof construction and learn from formal feedback.

报告人简介：

       李金政 (Jinzheng Li)，博士阶段在美国东北大学师从 Pran Nath 教授，即将加入韩国基础科学研究院宇宙理论物理中心粒子理论与宇宙学组（IBS-CTPU-PTC），担任 Senior Researcher。主要研究方向为粒子宇宙学，包括暗物质、隐扇区热历史、早期宇宙一阶相变及随机引力波，相关成果发表于 Physical Review D、JHEP 等期刊。
       近期研究进一步拓展至人工智能辅助的形式化证明，参与开发 MerLean 与 MerLean-Prover，探索利用大语言模型与 Lean 实现数学和理论物理研究中的自动形式化、定理证明与机器验证。