2026年09月29日 至 12月22日

No prior knowledge of artificial intelligence, machine learning, large language models, or formal theorem proving is required. Participants are expected to have mathematical maturity at the undergraduate level and some basic programming experience. Familiarity with Python is helpful but not necessary.

Course Calendar

Lecture 1: LLMs for Mathematical Research: APIs, Prompting, and Reproducible Workflows
Model and API basics; context management; token usage; batch inference; precise mathematical prompting; assumptions and specifications; structured outputs; critique and verification protocols; reproducible workflows and logging.

Lecture 2: Tool-Using Mathematical Agents
Python, shell, files, symbolic computation, function calling, and external mathematical software; integration with SymPy, SageMath, Mathematica, and numerical tools; computational experiments; theorem-search tools; reliable tool-use loops.

Lecture 3: Lean 4 for AI-Assisted Mathematics I: Foundations of Formal Proof
Propositions as types; terms and proofs; theorem statements; logical connectives; quantifiers; equality; basic tactics; rewriting; induction; translating ordinary mathematical statements into Lean.

Lecture 4: Lean 4 for AI-Assisted Mathematics II: Mathlib and Mathematical Structures
Mathlib organization; theorem search; namespaces; structures; typeclasses; algebraic hierarchies; sets and functions; finite sums; examples from algebra, analysis, combinatorics, and geometry.

Lecture 5: Lean 4 for AI-Assisted Mathematics III: Formalization Engineering
Designing definitions; choosing abstraction levels; mathematical APIs; lemma organization; coercions and typeclass issues; debugging; refactoring; formalizing substantial existing proofs; building maintainable Lean projects.

Lecture 6: LLM + Lean: Automated Formalization and Proof Search
Generating Lean statements and proofs with LLMs; compilation as verification; error-feedback loops; iterative proof repair; theorem retrieval; multiple proof candidates; tactic and term proofs; automated proof-search pipelines; reliability and evaluation.

Lecture 7: From Mathematical Proofs to Lemma DAGs
Proof decomposition; dependency graphs; lemma interfaces; bottleneck lemmas; recursive decomposition; discovering missing lemmas; restructuring proof plans; machine-readable proof states; coordinating automated proving through lemma DAGs.

Lecture 8: Multi-Agent and Large-Scale Theorem Proving
Planner-worker-verifier architectures; parallel proof attempts; strategy diversity; large-scale proof search; compute allocation; adaptive search over lemma DAGs; candidate ranking; verification; failure analysis.

Lecture 9: Persistent Mathematical Memory and Long-Horizon Agents
Storing verified lemmas, failed approaches, counterexamples, experiments, and provenance; retrieval systems; context compression; checkpointing; hierarchical agents; maintaining project state; reasoning across many sessions and beyond a single context window.

Lecture 10: Extracting Mathematical Theorems from Physics Papers
Turning physics literature into precise mathematical definitions, statements, conjectures, and theorem candidates; separating assumptions, heuristics, and proved results; reconstructing omitted derivations; translating physical arguments into mathematical language; identifying formalization targets; building dependency structures from scientific papers.

Lecture 11: Conjecture-Proof-Counterexample Systems
Conjecture generation; computational exploration; counterexample search; hypothesis refinement; experimental mathematics; symbolic and numerical evidence; automated proof attempts; formal verification; conjecture-test-repair-proof loops.

Lecture 12: AI-Native Mathematical Research Systems
Automated formalization; large-scale lemma generation; theorem retrieval and deduplication; mathematical knowledge bases; integration of LLMs, Lean, symbolic and numerical software, lemma DAGs, multi-agent search, and persistent memory; end-to-end AI-native research workflows and capstone projects.

As this is a rapidly developing subject, the course will mainly use online documentation, research papers, and software repositories rather than a single textbook.

[1] Lean Prover Community, Mathematics in Lean.
[2] Theorem Proving in Lean 4.
[3] The mathlib Community, Mathlib Documentation.
[4] Current documentation for major large language model APIs and agent frameworks.
[5] Selected recent papers on LLM-based theorem proving, formal mathematics, proof decomposition, and multi-agent mathematical reasoning.
[6] Selected documentation for mathematical software including SageMath, Mathematica, GAP, PARI/GP, FLINT, and related systems.

Undergraduate , Advanced Undergraduate , Graduate , 博士后 , Researcher

公开

公开

中文 , 英文