10100024 Computational Logic in the Era of AI

September 2026–December 2026

Monday, class 7–9·马池口110

Teaching assistants: Sijie Liang

Language models now produce code and mathematical proofs in quantity, but they offer no guarantee that what they produce is correct, and reviewing it by inspection does not scale. Formal verification provides such a guarantee: a specification states precisely what a program or a theorem must satisfy, and a proof that it does so can be checked mechanically by a small program, independently of how that proof was found. This course develops that idea from its foundations to its practical use. The theory begins with the untyped λ-calculus and builds through the λ-cube to the type theory on which Lean 4 rests, including the correspondence between propositions and types that makes proof checking a form of type checking. The practice begins with Lean as a programming language and ends with programs that carry contracts and machine-checked proofs of their specifications. On completing the course, students will be able to write formal specifications, prove that implementations satisfy them, and determine what an AI-generated program or proof does and does not guarantee.

September 2026

7
Mon

lecture

14
Mon

lecture

  • Simply Typed Lambda Calculus
21
Mon

lecture

  • The λ-Cube and Propositions-as-Types
28
Mon

lecture

  • Definitions, Environments, and the Trusted Core

October 2026

5
Mon

No class

12
Mon

lecture

  • Inductive Types, and What CIC Adds
19
Mon

lecture

  • Equality, and Sets as Predicates
26
Mon

lecture

  • Automation, and the Decidable Fragment

November 2026

2
Mon

lecture

  • Specification, Verification, and Testing
9
Mon

lecture

  • Effects and Monads
16
Mon

lecture

  • Hoare Logic
23
Mon

lecture

  • Weakest Preconditions
30
Mon

lecture

  • Loops, Invariants and Verification Conditions

December 2026

7
Mon

lecture

  • Verification-Condition Generation
14
Mon

lecture

  • Intrinsic Contracts
21
Mon

lecture

  • AI in the Loop