Month: November 2026

November 6, 2026

CSC 379/579 Logic Foundation and Machine-Checked Proofs

Spring 2027
(R 9:40am to 10:55 Wegmans 1005)

The language of intelligence is logic. The course teaches proof systems, with a focus on Rocq. You will learn to use Rocq to formalize logic, which is the fundamental language of rational thought and problem-solving, and construct sound and verifiable proofs. A similar system, Lean, was used in proving mathematical theorems. By learning the fundamentals of modern proof systems, you acquire a thorough grounding in logical thinking and the knowledge and skills to build or use automated reasoning systems.

Prerequisites: Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254, or 255) or mathematical logic.

Syllabus

  • The Need for Training Thought: The Values of Thought. Tendencies Needing Constant Regulation.  Regulation Transforms Inference into Proof.
  • Type Systems.  Syntax, semantics and types. Formal rules. Informal type soundness proof.
  • Functional Programming in Rocq: Data and Functions.  Proof by Simplification, Rewriting and Case Analysis.
  • Proof by Induction. Proofs Within Proofs.  Formal vs. Informal Proof.
  • Basic Tactics: apply, apply with, injection, discriminate, unfold, destruct.
  • Logical Connectives: Conjunction, Disjunction, Falsehood and Negation, Truth, Logical Equivalence, Logical Equivalence, Existential Quantification. 
  • Programming with Propositions. Applying Theorems to Arguments. Coq vs. Set Theory: Functional Extensionality, Propositions vs. Booleans, Classical vs. Constructive Logic.
  • Inductively Defined Propositions. Reasoning with Evidence: Destruct, Inversion, (Multi-)induction.
  • The Curry-Howard Correspondence. Natural Deduction. Typed Lambda Calculus. Proof Scripts. Quantifiers, Implications, Functions. Logical Connectives as Inductive Types.
  • (Time permitting) Induction Principles.

Textbooks

Related News

  • September 7, 2026: OpenAI announced that its internal AI system produced a proof of the Navier-Stokes existence and smoothness problem (one of the Millennium Prize Problems) and released the proof text and its formalization in Lean. Official report: https://openai.com/index/navier-stokes-solution/
  • October 21, 2026: Anthropic announced that Claude generated Rocq formal proofs for 239 entry points across 123 open-source libraries at the RISC-V assembly level, uncovering hundreds of vulnerabilities. Official report: https://www.anthropic.com/research/formal-verification
  • October 2026: DeepMind’s AlphaProof Nexus solved 9 previously open Erdős problems, with all proofs machine-verified using Lean. Paper link: https://www.science.org/doi/10.1126/science.aej2213