Courses
Proposed Objectives and Key Contents of New Courses for the Graduate School of AI Mathematics
개설교과목 (교과목 취지 및 주요 내용) - en
|
Course Category (Lecture:Practice:Credits) |
Course Title | Course Objectives and Main Contents |
|---|---|---|
|
Major Elective (Basic) (3:0:3) |
Introduction to Formalized Mathematics | This course covers foundational concepts for mathematical formalization, including dependent type-theoretic logic, the Curry-Howard correspondence, Lean 4 basic syntax, and the structure of mathlib, and reproduces proofs by formalizing undergraduate-level theorems (algebra, analysis). |
| Interactive (Conversational) Theorem Proving | This course explores Lean metaprogramming techniques, DSL design, user-defined tactics, and syntax extensions to understand the structure and principles of proof automation, and implements graduate-level mathematics (such as number theory and topology) through formalization to develop advanced concepts and techniques. | |
|
Major Elective (Advanced) (3:0:3) |
Automated Reasoning and Proof Search | This course covers classical logic-based automated reasoning techniques such as SAT, SMT, and DPLL, as well as proof structures in first-order logic and decision procedures in SMT theories, and analyzes automation strategies of Lean tactics (simp, aesop, linarith), with hands-on practice building a mini prover to learn proof search structures. |
| AI for Theorem Proving | This course covers AI-based theorem proving techniques, including proof structure embedding using GNNs and Transformers, reinforcement learning-based tactic search, and automatic problem formalization and proof generation using LLMs. | |
| AI-based Mathematical Discovery | This course explores recent research trends in discovering new mathematical phenomena, identifying open problems, and proving theorems using modern AI techniques (GNNs, Transformers, LLMs, symbolic computation), and develops research and technical skills through paper presentations and small-scale projects. |