English

Discrete mathematics studies structures built from distinct objects and relations: integers, sets, sequences, graphs, and logical statements. “Discrete” does not mean “finite”: the natural numbers form an infinite discrete domain. Its place in computer science comes from the questions it lets us formulate. Which states are reachable? How many arrangements are possible? What remains true after one more operation?

Its central contribution is a way to move from examples to justified general claims. Running a function on many lists can reveal mistakes; induction can explain why it works for every finite list satisfying its preconditions. The guarantee remains conditional on the model. A proof using unbounded integers does not by itself establish the behavior of a fixed-width implementation.

Basic algebra and familiarity with simple programs are enough to start. Learn definitions, examples, counterexamples, and proofs together. Calculus is not a prerequisite; neither must every proof technique be mastered before studying graphs or algorithms.

From Counting and Graphs to Program Proofs

The ingredients of discrete mathematics have different histories. Counting arrangements, reasoning about divisibility, and constructing logical arguments long predate computers. They were brought together in computing education because programs repeatedly produce questions about finite descriptions, discrete states, and structures defined by rules.

Euler’s treatment of the Königsberg bridges in 1736 illustrates a decisive modeling move. Replace land areas with vertices and bridges with edges; distances and shapes can be discarded because the question is whether a walk can use each edge exactly once. Each intermediate visit pairs an entering edge with a departing edge. Consequently, an undirected graph with all its non-isolated vertices connected has an Euler circuit when every vertex has even degree, or an open Euler trail when exactly two have odd degree. Königsberg’s four odd-degree vertices rule out either possibility. The insight is not merely a theorem about bridges: selecting what to leave out made the proof possible.

Nineteenth- and twentieth-century logic supplied formal languages for propositions, quantifiers, and inference. Computing then made these subjects practical in new ways: Boolean operations became useful in switching circuits, recursive definitions described data and procedures, and assertions helped reason about program execution. Floyd’s and Hoare’s work in the 1960s made the link between program structure and proof especially explicit.

Number theory followed another route into computing through efficient arithmetic and cryptography. Its theorems do not automatically make a cryptosystem secure: security also depends on a precisely stated computational problem, an adversary model, and the protocol. Across these histories, the recurring contribution is a disciplined representation that makes a useful question answerable.

Proof, Structure, and the Discipline of Precision

A definition chooses the objects and relationships under discussion; a theorem states what follows; a proof explains why. Keeping these roles separate prevents a common mistake: treating a suggestive picture or a successful example as if it established the general result. Pictures and experiments are valuable for discovering a claim, but the eventual argument must cover the domain stated in it.

Finite Arguments About Infinite Domains

Induction turns a repeated construction into a finite argument. To prove a property for every natural number, establish a starting case and show that the property passes from a case to its successor. Structural induction follows the constructors of a recursively defined object, such as an empty list and a list extended by one element.

The program that sums a list gives a concrete example. After i iterations, let the assertion be: 0 ≤ i ≤ n, and the accumulator equals the sum of the first i elements. Initialization establishes it at zero; adding the next element preserves it. When the loop exits at i = n, the assertion gives the result. The nonnegative quantity n - i decreases at each iteration, proving termination. The invariant explains preservation; the decreasing quantity explains progress. Neither does the other’s job.

Choosing the assertion is often harder than the induction itself. “The final answer is correct” says too little about an intermediate state. Adding bounds on the index and a description of the processed prefix makes the argument possible. Strengthening a claim can therefore make it easier to prove.

A tree shows how recursive definitions, programs, and proofs fit together. Define a finite full binary tree as either a leaf or a node joining two such trees. A leaf has no children; every other node has exactly two. A leaf-counting function can follow the definition: return 1 for a leaf, otherwise recursively count each child tree and add the results. Each call handles a smaller tree, so the definition also supplies a termination argument.

Now prove that every such tree has one more leaf than internal node. A single leaf has one leaf and zero internal nodes. If the two child trees have I₁ and I₂ internal nodes, the induction hypotheses give I₁ + 1 and I₂ + 1 leaves. Joining them adds one internal node and no leaves: the totals are I₁ + I₂ + 1 internal nodes and I₁ + I₂ + 2 leaves. The property follows for the joined tree. The recursive construction tells us both which subproblems a program must solve and which hypotheses a proof may use; it does not make an arbitrary recursive program correct.

Other techniques serve different structures. A contradiction argument assumes a claim’s negation and derives an impossibility. Euclid’s argument about primes constructs one more than a product of a proposed finite list of all primes. The new number need not be prime; a prime divisor absent from the list is enough. This distinction is a useful exercise in reading what a proof actually requires.

Logic as the Language of Precision

Logic makes the scope of a claim visible. “For every input, there exists a memory bound sufficient for that input” differs from “there exists one memory bound sufficient for every input.” Reversing the quantifiers changes the requirement from finite use on each instance to a uniform bound over all instances. Many specification errors have this form even when no logical symbols appear in the code.

Implication also needs care: from “if the input satisfies the precondition, the output has property Q,” nothing follows about inputs outside the precondition. An empty collection can satisfy “every member has property Q” without containing any members. Testing definitions on empty, singleton, and boundary cases exposes these issues early.

Sets express membership, relations express connections, and functions associate each permitted input with one output. A relation need not be a function: a user may have several roles. Distinguishing these structures is directly useful when choosing a schema or an interface. Formal notation earns its place by exposing a decision that ordinary wording left ambiguous.

Counting and Structure

Counting can establish limits before any implementation exists. There are 2^n binary strings of length n, but only 2^n - 1 binary strings of all shorter lengths combined. An injective encoding therefore cannot shorten every n-bit string. Lossless compression succeeds by exploiting a restricted or nonuniform source, not by defeating this count.

The pigeonhole principle gives deterministic conclusions: more items than bins force a shared bin. The birthday problem asks a different question. For 23 independent, uniformly distributed birthdays among 365 days, the probability of at least one collision is 1 - (365 × 364 × … × 343) / 365^23, about 50.7%. A collision is probable, not inevitable. The result comes from counting and a probability model, not from the pigeonhole principle alone.

Graphs record relationships: directed edges can express dependencies; paths express reachability; a topological ordering exists precisely when a finite directed graph has no directed cycle. Recurrences describe recursive work, while modular arithmetic describes quantities up to a modulus. The extended Euclidean algorithm, for example, finds an inverse of a modulo m when gcd(a, m) = 1; the modulus need not be prime. In each case, choosing the structure makes an algorithm or a limitation easier to see.

What Studying This Changes

The payoff is a more deliberate reading of claims. Ask for the domain, the quantifiers, the assumptions, and a possible counterexample. When reviewing an algorithm, try to name the property preserved by its steps; when reviewing a data model, ask whether its relationships have been represented faithfully.

A useful learning test combines several activities: define a small structure, draw examples and a counterexample, implement an operation, and justify one property of it. For a dependency graph, that might mean distinguishing a path from a cycle and explaining why a proposed processing order respects every edge. The goal is transferable reasoning, not reproducing a catalog of famous proofs.

Resources

Books and Texts

The current canonical entry is Lehman, Leighton, and Meyer’s Mathematics for Computer Science (MIT 6.042J, free PDF), developed for MIT’s introductory mathematics course for CS students. The book’s distinguishing feature is that it treats proof technique as the central subject rather than as background: the first substantial chapter is about proofs, and the mathematical content (number theory, graph theory, probability, counting) is developed within a framework that constantly asks how claims are established, not just what the claims are. It is unusually well-written for the genre, with a direct voice that takes the philosophical content of mathematical reasoning seriously. The companion MIT 6.042J lectures (free on MIT OpenCourseWare and YouTube) are of high quality and are worth using alongside the text, especially for topics where a worked example helps more than additional reading.

For learners whose specific bottleneck is proof construction — who can follow definitions and theorems but cannot produce arguments themselves — Velleman’s How to Prove It (3rd ed., 2019) is the most focused intervention available. It isolates proof technique from mathematical content, working through the logical structure of mathematical statements (what does it mean to prove an implication? a universal statement? an existential?), the major proof strategies, and the process of translating informal arguments into rigorous ones. It is narrower than MCS — it does not cover combinatorics, graph theory, or probability — but for the learner who needs to build proof skill specifically, it addresses the bottleneck directly. Reading Velleman then MCS is a reliable path for learners who find MCS’s pace too fast.

Oscar Levin’s Discrete Mathematics: An Open Introduction (free online) is a gentler open textbook with many exercises, hints, and solutions. It is especially useful for readers who need more runway before MIT MCS or who want an accessible second explanation of counting, induction, relations, functions, and graph basics. It is less CS-oriented and less complete than MCS, so it should be used as auxiliary support rather than as the main spine.

Richard Hammack’s Book of Proof (free online) is a clean bridge into proof-writing. It does not replace Velleman, but its direct style, exercises, and low barrier to entry make it useful for learners who need repeated practice translating mathematical intuition into written proof.

Rosen’s Discrete Mathematics and Its Applications (8th ed.) is comprehensive and example-rich and is used in many undergraduate programs. Its weakness is that its writing is competent without being illuminating: it covers material without giving the reader a strong sense of why the material coheres or what kind of thinking it is building. It is better as a reference — to look up a specific topic or find additional worked examples — than as a primary text for self-directed learners.

For combinatorics at depth, Graham, Knuth, and Patashnik’s Concrete Mathematics is the canonical extension. Written specifically for algorithm analysis, it develops sums, recurrences, generating functions, and asymptotic notation with far more depth than introductory texts. The book is also genuinely entertaining — Knuth’s personality is visible throughout — and can be read after MCS by any learner planning serious algorithm analysis. It is one of the few mathematics books that is both technically demanding and a pleasure to read.

For graph theory at depth, Diestel’s Graph Theory (5th ed., free online) is the modern standard for rigorous treatment. Bondy and Murty’s Graph Theory is an alternative with broader problem coverage. Either is appropriate after introductory exposure for learners whose work involves networks, algorithms on graphs, or combinatorial optimization.

Pólya’s How to Solve It is the heterodox text that belongs alongside the technical curriculum. It is about the heuristics of mathematical problem-solving — what to do when the approach is not clear, how to specialize and generalize, when to work backward, how to use analogy — and these heuristics are applicable at every level of mathematical sophistication. It does not teach discrete mathematics, but it teaches the thinking style that makes discrete mathematics learnable and productive. Reading it alongside MCS improves performance on hard problems. Proofs from THE BOOK (Aigner and Ziegler) is a different kind of supplement: a collection of particularly elegant proofs with no pedagogical intent beyond demonstrating what mathematical beauty looks like. Exposure to elegant proofs develops mathematical taste, and mathematical taste influences which approaches a practitioner reaches for first.

Book Role Type
Lehman, Leighton, Meyer, Mathematics for Computer Science (free) Current canonical entry Entry
Velleman, How to Prove It (3rd ed.) Focused proof-technique entry Entry
Levin, Discrete Mathematics: An Open Introduction (free) Gentle open discrete math entry Auxiliary
Hammack, Book of Proof (free) Proof-writing bridge for beginners Auxiliary
Rosen, Discrete Mathematics and Its Applications Comprehensive reference Reference
Graham, Knuth, Patashnik, Concrete Mathematics Combinatorics and asymptotics at depth Depth
Diestel, Graph Theory (free online) Graph theory at depth Depth
Selected chapters from Mitzenmacher & Upfal, Probability and Computing Probabilistic methods for algorithms Depth
Pólya, How to Solve It Problem-solving heuristics Auxiliary
Aigner & Ziegler, Proofs from THE BOOK Mathematical taste and elegance Auxiliary
Hardy, A Mathematician’s Apology Philosophy of mathematical work Auxiliary

Courses and Lectures

MIT 6.042J is the course from which the MCS text emerged. Full lecture videos are freely available on MIT OpenCourseWare and YouTube, with problem sets and exams. For self-learners, the course provides pacing and worked examples that the text alone does not, and the combination of book and lectures is substantially more effective than either alone.

MIT 6.042J on OCW covers a slightly different syllabus from the most recent textbook edition; reading them together and reconciling the differences is itself a useful exercise in mathematical flexibility. The lectures emphasize different aspects than the text at various points, which means watching lectures on a topic after reading about it often resolves confusions that additional reading would not.

For combinatorics specifically, the lectures from MIT 18.212 (Algebraic Combinatorics) and Stanford’s CS 70 (Discrete Mathematics and Probability Theory) offer alternative expositions at comparable level. CS 70 is particularly strong on the probability material and on the connection between combinatorics and computation.

Course Platform Type
MIT 6.042J lectures + problem sets (free) MIT OCW / YouTube Entry
Stanford CS 70 Discrete Math and Probability (free) Stanford / YouTube Entry

Practice, Tools, and Code

3Blue1Brown (YouTube) has no single video on discrete mathematics as a subject, but videos on topics that appear in it — linear transformations, set theory intuitively, combinatorics problems — are unusually good at building geometric and visual intuition before the algebra. Watching the relevant videos before engaging with a textbook topic often makes the formalism feel like a description of something already partially understood rather than a definition of something entirely new.

Lean and Coq are proof assistants — software systems in which mathematical proofs are written as programs and mechanically verified. Working through even simple proofs in Lean changes how proof feels: the system forces complete precision, accepts no hand-waving, and provides immediate feedback when a step is invalid. The Lean community’s Mathematics in Lean (free, online tutorial) is the accessible entry point. Engaging with a proof assistant while learning discrete mathematics — even for a small fraction of the exercises — is one of the most effective ways to internalize what proof actually requires. It also connects forward to §3.6 (Formal Methods and Proof Assistants), where these tools are treated at depth.

The Xena Project (Kevin Buzzard, Imperial College) is formalizing undergraduate mathematics in Lean and making the results available online. Browsing formalized proofs of theorems one has just proved informally — seeing how the informal argument maps to the formal one — is illuminating in ways that no textbook description of proof assistants can replicate.

Resource Platform Type
3Blue1Brown (selected topics, free) YouTube Practice
Lean / Mathematics in Lean (free) leanprover-community.github.io Practice
Xena Project / Mathlib (free) leanprover-community.github.io/mathlib4 Practice

Traps

Trap Why it misleads Better response
Treating examples as proof A finite sample may miss a whole class of cases. Use examples to discover a claim, then identify an argument covering its stated domain.
Memorizing a proof’s sentences Recall does not reveal why the argument works. Change an assumption and locate the step that now fails.
Applying induction mechanically The obvious assertion may be too weak to support the next step. State what the recursive call or next iteration actually needs; strengthen the invariant accordingly.
Using symbols without checking scope Quantifier order and preconditions can change the claim. Translate the statement into plain language and test empty and boundary cases.
Confusing certainty with probability A forced collision and a likely collision are different conclusions. State whether the argument is combinatorial or probabilistic and name its assumptions.
Accepting an assisted proof without understanding it Fluent wording can conceal a missing case or an invalid inference. Reconstruct the argument and solve a nearby variant independently; use tools to challenge specific steps.

中文

离散数学研究由可区分的对象及其关系组成的结构:整数、集合、序列、图和逻辑命题。“离散”不等于“有限”:自然数就是无限的离散领域。它在计算机科学中的位置,来自它帮助我们提出的问题:哪些状态可以到达?有多少种排列方式?再执行一次操作后,什么性质仍然成立?

它的核心贡献,是提供从实例走向有根据的一般结论的方法。在许多列表上运行函数可以发现错误;归纳法则能解释,为什么它对所有满足前提的有限列表都有效。这种保证仍以模型为条件:使用无界整数的证明,本身并不能保证定长整数实现具有相同行为。

掌握基础代数、熟悉简单程序就可以开始。把定义、实例、反例与证明一起学习。微积分不是前置条件,也不必先熟练掌握全部证明技巧,才能接触图或算法。

从计数与图到程序证明

离散数学的各个组成部分有不同的历史。计数、整除关系和逻辑论证都远早于计算机。计算教育把它们组织在一起,是因为程序不断产生关于有限描述、离散状态和规则所定义的结构的问题。

Euler 在 1736 年对哥尼斯堡七桥问题的处理,展示了一次关键的建模选择。把陆地区域换成顶点,把桥换成边;距离与形状可以舍去,因为问题只问能否走出一条恰好经过每条边一次的路线。每次中途经过一个顶点,进入和离开的边都要成对出现。因此,对所有非孤立顶点连通的无向图,每个顶点的度数都为偶数时存在欧拉回路;恰有两个奇度顶点时存在不闭合的欧拉通路。哥尼斯堡的四个奇度顶点排除了这两种可能。其启发不只是一个关于桥的定理:恰当地选择忽略什么,使证明成为可能。

十九、二十世纪的逻辑研究为命题、量词与推理提供了形式语言。计算又赋予这些研究新的实际用途:布尔运算用于开关电路,递归定义用于描述数据与过程,断言用于推理程序执行。二十世纪六十年代 Floyd 和 Hoare 的工作,尤其明确地建立了程序结构与证明之间的联系。

数论则经由高效算术和密码学进入计算。数论定理不会自动使密码系统安全:安全性还依赖精确定义的计算问题、攻击者模型以及协议本身。这些历史反复显示的贡献,是用经过推敲的表示,让有用的问题变得可以回答。

证明、结构与精确性的纪律

定义选定讨论的对象与关系,定理陈述由此能够得到的结论,证明解释结论为什么成立。分清这三种角色,可以避免一种常见错误:把富有启发的图像或成功实例当成一般结论的依据。图像与试验有助于发现命题,但最终的论证必须覆盖命题所声称的范围。

关于无限领域的有限论证

归纳法把反复进行的构造变成有限的论证。要证明一个性质对所有自然数成立,先建立起始情形,再说明它能从一个情形传递到后继情形。结构归纳则遵循递归对象的构造方式,例如空列表,以及在列表上增加一个元素。

列表求和程序提供了一个具体例子。执行 i 次循环后的断言可以是:0 ≤ i ≤ n,且累加器等于前 i 个元素的和。初始化使它在零处成立;加入下一个元素后,它仍成立。循环在 i = n 时退出,断言便给出所需结果。非负量 n - i 每次迭代都减小,因此程序会终止。不变式解释性质如何保持,递减量解释执行如何取得进展;两者不能相互替代。

选择断言往往比归纳步骤本身更难。“最终答案正确”没有充分描述中间状态。补上索引范围与已处理前缀的含义,论证才有了抓手。因此,加强命题有时反而使它更容易证明。

树可以说明递归定义、程序与证明怎样配合。规定一种有限二叉树:它或者是一片叶子,或者是用一个节点连接两棵这样的树。叶子没有子节点,其余节点都恰有两个子节点,英文称为 full binary tree。计算叶子数的函数可以沿着定义写:遇到叶子返回 1,否则递归计算两棵子树的叶子数并相加。每次递归调用处理的树都更小,因此这个定义也提供了终止论证。

现在证明:这样的树,叶子数总比内部节点数多一。单个叶子具有一片叶子、零个内部节点。如果两棵子树分别有 I₁、I₂ 个内部节点,归纳假设便给出 I₁ + 1、I₂ + 1 片叶子。连接它们只增加一个内部节点,不增加叶子,所以总计有 I₁ + I₂ + 1 个内部节点、I₁ + I₂ + 2 片叶子,性质对连接后的树仍成立。递归构造既告诉程序要处理哪些子问题,也告诉证明可以使用哪些归纳假设;它并不使任意递归程序自动正确。

其他方法适用于不同结构。反证法假定命题的否定,并由此推出矛盾。Euclid 关于素数的论证,把假定列全的有限个素数相乘,再加一。这个新数不一定是素数;只要它具有一个不在原列表中的素因子就够了。分清这一点,是练习读懂证明实际需要什么的好例子。

逻辑是精确性的语言

逻辑使命题的作用范围变得清楚。“对每个输入,都存在一个足以处理它的内存上界”,不同于“存在同一个内存上界,足以处理所有输入”。调换量词,就把逐个实例的有限用量要求,变成了对所有实例统一的上界要求。即使代码没有出现逻辑符号,许多规格错误也具有这种形式。

蕴涵同样需要小心:从“如果输入满足前置条件,输出就具有性质 Q”,不能推断前置条件之外的输入会怎样。空集合可以满足“每个成员都具有性质 Q”,却一个成员也没有。用空值、单元素和边界情形检查定义,有助于尽早暴露这些问题。

集合表达成员关系,关系表达对象间的联系,函数则把每个允许的输入对应到唯一输出。关系不一定是函数:一个用户可以拥有多个角色。选择数据模式或接口时,分清这些结构很有用。形式记号的价值,在于揭示普通措辞掩盖了的选择。

计数与结构

计数能在实现出现之前建立边界。长度为 n 的二进制串有 2^n 个,而所有更短的二进制串加在一起只有 2^n - 1 个。因此,保持一一对应的编码不可能缩短每个 n 位串。无损压缩之所以有效,是利用了受限或非均匀的信息来源,而不是突破了这个计数结论。

鸽巢原理给出确定性结论:物品多于盒子,就必有物品共用一个盒子。生日问题问的是另一件事。如果 23 个人的生日相互独立,且均匀分布在 365 天中,至少一次碰撞的概率是 1 - (365 × 364 × … × 343) / 365^23,约为 50.7%。碰撞是很可能发生,而不是必然发生。这一结论来自计数与概率模型,不能单靠鸽巢原理得到。

图记录对象间的关系:有向边可以表达依赖,路径表达可达性;有限有向图存在拓扑序,当且仅当它没有有向环。递推关系描述递归工作的规模,模运算描述按某个模数区分的量。例如,扩展 Euclid 算法在 gcd(a, m) = 1 时能求出 a 模 m 的逆元;模数不必是素数。在这些例子中,选对结构,就更容易看见算法或限制。

学习这一部分会改变什么

收获是更有意识地阅读各种主张:追问定义域、量词、前提,以及可能的反例。审阅算法时,试着说出各步骤保持的性质;审阅数据模型时,检查其中的关系是否得到了忠实表示。

一个实用的学习检验可以结合几种活动:定义一个小结构,画出实例和反例,实现一个操作,再论证它的一项性质。以依赖图为例,可以区分路径与环,并解释为什么某个处理顺序符合每条边的要求。目标是能够迁移的推理能力,而不是复述一套著名证明。

资源

书籍与文本

当前的经典入口,是 Lehman、Leighton 和 Meyer 的 Mathematics for Computer Science(MIT 6.042J,免费 PDF),这本书是为 MIT 面向 CS 学生的入门数学课程开发的。它的独特之处在于,它把证明技术当作中心主题,而不是背景知识:第一个实质性章节就是关于证明的;而数学内容(数论、图论、概率、计数)都是在一个不断追问“这些主张如何被建立”的框架中展开,而不只是说明“这些主张是什么”。对于这一类教材来说,它写得异常好,声音直接,并且认真对待数学推理中的哲学内容。配套的 MIT 6.042J 讲座(可在 MIT OpenCourseWare 和 YouTube 免费获取)质量很高,值得与教材一起使用;尤其在那些看一个完整例子比继续读更多文字更有帮助的主题上,讲座很有价值。

对于那些具体瓶颈在证明构造上的学习者——也就是能读懂定义和定理,却不能自己写出论证的人——Velleman 的 How to Prove It(第 3 版,2019)是目前最集中的干预工具。它把证明技术从数学内容中分离出来,逐步处理数学陈述的逻辑结构(证明一个蕴含意味着什么?证明一个全称命题意味着什么?证明一个存在命题意味着什么?)、主要证明策略,以及把非形式论证翻译成严密论证的过程。它比 MCS 更窄——不覆盖组合数学、图论或概率——但对于需要专门建立证明能力的学习者,它直接处理瓶颈。先读 Velleman,再读 MCS,是觉得 MCS 节奏太快的学习者的一条可靠路径。

Oscar Levin 的 Discrete Mathematics: An Open Introduction(免费在线)是一本更温和的开放教材,包含大量练习、提示和解答。它特别适合那些在进入 MIT MCS 前需要更多跑道的读者,也适合作为计数、归纳、关系、函数和图基础的第二种解释。它的 CS 导向不如 MCS,完整性也不如 MCS,因此更适合作为辅助支持,而不是主干教材。

Richard Hammack 的 Book of Proof(免费在线)是进入证明写作的清晰桥梁。它不能替代 Velleman,但它直接的风格、练习和较低进入门槛,使它非常适合那些需要反复练习把数学直觉翻译成书面证明的学习者。

Rosen 的 Discrete Mathematics and Its Applications(第 8 版)内容全面、例子丰富,被许多本科项目采用。它的弱点在于,写作合格但不够启发:它覆盖材料,却没有给读者很强的感觉,让人理解这些材料为什么组成一个整体,或者它正在训练哪种思维。它更适合作为参考书——查某个具体主题,或找额外例题——而不是自学者的主要文本。

对于深入学习组合数学,Graham、Knuth 和 Patashnik 的 Concrete Mathematics 是经典延伸。它专门为算法分析而写,以远超入门教材的深度发展求和、递推、生成函数和渐近记号。这本书也确实有趣——Knuth 的个性贯穿其中——任何计划认真学习算法分析的学习者,都可以在 MCS 之后阅读它。它是少数既技术要求高、又读起来有乐趣的数学书之一。

对于深入学习图论,Diestel 的 Graph Theory(第 5 版,免费在线)是严谨处理图论的现代标准。Bondy 和 Murty 的 Graph Theory 是另一个选择,题目覆盖更广。对于那些工作涉及网络、图算法或组合优化的学习者来说,在入门之后阅读其中任何一本都是合适的。

Pólya 的 How to Solve It 是一本文本取向不同、但应该与技术课程并列的异端书。它讨论的是数学解题的启发法——当方法不清楚时该做什么,如何特殊化和一般化,什么时候倒推,如何使用类比——这些启发法适用于各种数学成熟度层次。它不教授离散数学,但它教授一种思维风格,使离散数学更容易学习、更有生产力。把它与 MCS 一起阅读,会提高处理难题的能力。Proofs from THE BOOK(Aigner 和 Ziegler)是另一种补充:它收集特别优雅的证明,并不以教学为主要目的,而是展示数学之美。接触优雅证明会发展数学品味,而数学品味会影响实践者首先尝试哪些方法。

书籍 作用 类型
Lehman, Leighton, Meyer, Mathematics for Computer Science(免费) 当前经典入口 入门
Velleman, How to Prove It(第 3 版) 专门训练证明技术的入口 入门
Levin, Discrete Mathematics: An Open Introduction(免费) 温和的开放离散数学入口 辅助
Hammack, Book of Proof(免费) 面向初学者的证明写作桥梁 辅助
Rosen, Discrete Mathematics and Its Applications 综合参考 参考
Graham, Knuth, Patashnik, Concrete Mathematics 深入组合数学与渐近分析 深入
Diestel, Graph Theory(免费在线) 深入图论 深入
Mitzenmacher & Upfal, Probability and Computing 选章 面向算法的概率方法 深入
Pólya, How to Solve It 解题启发法 辅助
Aigner & Ziegler, Proofs from THE BOOK 数学品味与优雅证明 辅助
Hardy, A Mathematician’s Apology 数学工作的哲学 辅助

课程与讲座

MIT 6.042J 是 MCS 教材所来源的课程。完整讲座视频可在 MIT OpenCourseWare 和 YouTube 免费获取,并配有习题和考试。对自学者来说,这门课提供了教材本身不具备的节奏感和完整例题;教材与讲座结合起来,效果明显强于单独使用其中任何一个。

MIT 6.042J on OCW 的大纲与最新版教材略有不同;把二者一起阅读,并调和其中差异,本身就是一种有用的数学灵活性练习。讲座在不同主题上强调的侧面与教材不同,这意味着读完某个主题后再看讲座,往往能解决继续阅读无法解决的困惑。

对于组合数学本身,MIT 18.212(Algebraic Combinatorics)和 Stanford CS 70(Discrete Mathematics and Probability Theory)的讲座提供了相近层次的不同讲法。CS 70 在概率材料,以及组合数学与计算之间的连接上尤其强。

课程 平台 类型
MIT 6.042J lectures + problem sets(免费) MIT OCW / YouTube 入门
Stanford CS 70 Discrete Math and Probability(免费) Stanford / YouTube 入门

实践、工具与代码

3Blue1Brown(YouTube)并没有一个专门讲离散数学整体的单一视频,但它关于其中若干主题的视频——线性变换、直观集合论、组合数学问题——非常擅长在代数之前建立几何和视觉直觉。在接触教材主题之前观看相关视频,常常会让形式化内容感觉像是在描述某种已经部分理解的东西,而不是在从零定义一个完全陌生的东西。

Lean 和 Coq 是证明助手——在其中,数学证明会像程序一样被书写,并由机器进行验证。哪怕只是在 Lean 中完成一些简单证明,也会改变证明给人的感觉:系统要求完全精确,不接受任何含糊跳步,并在步骤无效时立刻给出反馈。Lean 社区的 Mathematics in Lean(免费在线教程)是可访问的入口。在学习离散数学时接触证明助手——哪怕只完成一小部分练习——也是内化“证明到底要求什么”的最有效方式之一。它还会向前连接到 §3.6(形式化方法与证明助手),那里会深入处理这些工具。

Xena Project(Kevin Buzzard,Imperial College)正在用 Lean 形式化本科数学,并在线提供相关成果。浏览那些你刚刚用非形式方式证明过的定理的形式化证明——看到非形式论证如何映射到形式化论证——能带来任何关于证明助手的教材描述都无法复制的启发。

资源 平台 类型
3Blue1Brown(选定主题,免费) YouTube 实践
Lean / Mathematics in Lean(免费) leanprover-community.github.io 实践
Xena Project / Mathlib(免费) leanprover-community.github.io/mathlib4 实践

陷阱

陷阱 为什么会误导 更好的做法
把实例当作证明 有限样本可能漏掉整类情形。 用实例发现命题,再寻找覆盖所声明范围的论证。
背诵证明的句子 记住文字不等于知道论证为什么成立。 改变一个前提,找出哪一步随之失效。
机械套用归纳法 最直观的断言可能太弱,无法支持下一步。 说明递归调用或下次迭代实际需要什么,据此加强不变式。
使用符号却不检查范围 量词顺序和前置条件都可能改变命题。 用普通语言重述,并检查空值和边界情形。
混淆必然性与概率 被迫发生的碰撞与很可能发生的碰撞是不同结论。 说明论证属于计数还是概率,并列出前提。
接受辅助生成的证明却没有理解 流畅措辞可能掩盖遗漏情形或无效推理。 重建论证,独立解决相近变式,并用工具质疑具体步骤。