English

Computer science was born from mathematics and has never left home, but the relationship between the two has grown into something more complicated than parent and child. Mathematics gave computer science its foundations — logic, the theory of computation, the analysis of algorithms, the structures that everything is built on — and the debt is enormous and permanent. But computer science is not applied mathematics, and the difference between how the two disciplines think is as important as the debt. And the relationship has become a dialogue: computer science now gives back to mathematics, reshaping what mathematicians do and even what they consider a proof. The relationship has three dimensions — what computer science owes mathematics, how the two differ despite the debt, and how they now influence each other — and understanding all three is necessary to understand either field’s place relative to the other.

The reason this relationship deserves its own examination, rather than being absorbed into the foundational chapters that use the mathematics, is that the boundary between the two fields is where some of the deepest questions about both live. Is computer science a branch of mathematics, or a distinct discipline that uses mathematics? What is the relationship between a mathematical proof and a computer program — are they the same kind of object, as some deep results suggest, or fundamentally different? When a proof is too long for any human to check but a computer can verify it, is it still a proof? These questions are not idle; they bear on what each field is, how it should be practiced, and what its results mean. They are visible only from the boundary, which is why the boundary is worth examining directly.

This section is not a mathematics tutorial — the mathematics that computer science uses is in the foundational chapters (§2.2–§2.6 for the core, §3.1–§3.3 for logic and computation theory). It is an examination of the relationship between the disciplines: the debt, the difference, and the dialogue. It assumes the reader has encountered the mathematics and asks what its relationship to computer science actually is.

Background: Discrete mathematics (§2.2), theory of computation (§3.2), complexity (§3.3), logic (§3.1), and type theory (§3.5) make this relationship legible; the focus here is how those areas connect, not a second presentation of their content.

The Relationship: What CS Owes, How It Differs, and How It Gives Back

The Debt

The debt computer science owes mathematics is foundational in the literal sense: the foundations of computing are mathematical, and they were laid by mathematicians, often before computers existed.

The theory of computation — the definition of what is computable, the proof that some things are not, the classification of problems by difficulty — is mathematics, developed in the 1930s by Gödel, Church, Turing, and Kleene as a branch of mathematical logic, before there were computers to run the computations they characterized. Turing’s machine was a mathematical abstraction defined to answer a question in the foundations of mathematics (Hilbert’s Entscheidungsproblem); that it became the conceptual basis for the physical computer was a consequence, not the intent. The lambda calculus, Church’s alternative formalization, was likewise a contribution to mathematical logic that became the basis for functional programming and the theory of programming languages. The deepest foundations of computer science are theorems in mathematical logic.

The analysis of algorithms is mathematics: the asymptotic notation, the recurrence relations, the probabilistic analysis, the combinatorial counting that determine how much time and space an algorithm requires are mathematical techniques, and the field of algorithm analysis is a branch of applied mathematics. Cryptography rests on number theory — the difficulty of factoring, the structure of finite fields and elliptic curves — that was pure mathematics, pursued for its own sake, long before it secured the internet. Machine learning rests on linear algebra, probability, optimization, and statistics; the mathematics is not incidental to it but constitutive of it. Graphics rests on linear algebra and the calculus of light transport. Across the field, the pattern repeats: the substance of each area, beneath the engineering, is mathematics.

The debt is not merely historical. Mathematics continues to be the language in which computer science’s deepest results are stated and proved, the source of the tools that new areas reach for, and the standard of rigor that the theoretical parts of the field hold themselves to. A theoretical computer scientist is a kind of mathematician; the proofs in a complexity theory paper are mathematical proofs, held to mathematical standards. The debt is ongoing and permanent: computer science draws on mathematics continuously, and the relationship is not one of a child who has grown independent but of a discipline whose foundations remain mathematical.

The Difference

Despite the debt, computer science is not mathematics, and the difference in how the two disciplines think is real and important. The difference is not about subject matter — they overlap heavily — but about orientation: what each field is trying to do, what it values, and what counts as progress.

Mathematics is oriented toward truth and understanding: the goal is to prove theorems, to understand why they are true, to find the structures and patterns that organize a domain of mathematical objects. The mathematician seeks the proof not merely to know that a thing is true but to understand why, and the value of a proof is partly in the understanding it provides. Computer science, even in its theoretical parts, is oriented toward computation and construction: the goal is often to build something, to find an algorithm, to make something work, and the theoretical results are frequently in service of this. The computer scientist analyzing an algorithm wants to know whether it is fast enough, which is a different question, with a different kind of answer, than the mathematician’s why.

This orientation produces differences in style and value. Computer science cares about constructive results — results that not only prove something exists but provide a way to build it — more than mathematics traditionally has, because a non-constructive proof that an algorithm exists does not give you the algorithm. Computer science cares about efficiency — not just whether something can be done but how much it costs — in a way that pure mathematics often does not, because the cost is the point when the goal is to actually compute. Computer science is more comfortable with the approximate, the heuristic, the probabilistic, the empirically-validated, because these often suffice for building things that work, whereas mathematics traditionally holds to the exact and the proven. The two fields share techniques and overlap in content, but the computer scientist and the mathematician are doing different things with them, and the difference is visible in what they consider a satisfying result.

The difference is sharpest around the role of proof and the role of experiment. Mathematics is a proof discipline: a result is established when it is proved, and experiment (computing examples, checking cases) suggests results but does not establish them. Computer science has a substantial experimental culture: systems are built and measured, algorithms are implemented and benchmarked, hypotheses about behavior are tested empirically, and much of the field’s knowledge is established experimentally rather than proved. This is not a deficiency — many of computer science’s questions (does this system perform well under real load? does this heuristic work on real inputs?) are not the kind that can be proved and must be investigated empirically. But it makes computer science a different kind of discipline from mathematics: part mathematical, part experimental, part engineering, in a combination that is its own rather than any of its parts.

The Dialogue

The relationship has become bidirectional: computer science now gives back to mathematics, in ways that are reshaping mathematical practice and even mathematical foundations.

The most direct gift is computation as a tool for mathematics. Computers let mathematicians explore, compute examples, test conjectures, and discover patterns at a scale impossible by hand. Experimental mathematics — the use of computation to investigate mathematical questions empirically, to generate conjectures and gather evidence for them — is a growing practice that computer science made possible. Some famous results were found or verified by computation: the Four Color Theorem was proved in 1976 with a proof that required a computer to check thousands of cases, and could not be verified by a human in full, raising the question of whether a proof no human can fully check is a proof — a question that computer science forced mathematics to confront.

The deeper gift is conceptual: computer science has contributed ideas and frameworks that have changed how mathematics is done and understood. Proof assistants — software systems (Coq, Lean, Isabelle) in which mathematical proofs are formalized and checked by computer — have grown from a curiosity into a serious tool, used to verify proofs too complex for confident human checking (the formal verification of the Four Color Theorem, the Feit-Thompson theorem, and recent work formalizing frontier research mathematics). The Lean theorem prover has attracted a community of mathematicians formalizing substantial mathematics, and Fields Medalist Terence Tao and others have used it on research-level work. This is computer science changing mathematical practice: the proof assistant, a computer science artifact, is becoming part of how some mathematics is done and verified.

The deepest dialogue is at the level of foundations, through the Curry-Howard correspondence and its descendants. The Curry-Howard correspondence (§3.5) — the discovery that proofs and programs are the same kind of object, that a proof of a proposition is a program of the corresponding type — revealed a profound identity between logic and computation that belongs to both fields and to neither alone. Its modern development, homotopy type theory and the univalent foundations program (initiated by the mathematician Vladimir Voevodsky, himself drawing on type theory from computer science), proposes a new foundation for mathematics based on type theory rather than set theory — a foundation in which the computer science notion of type is primary, and in which proofs are inherently computational and checkable. This is the dialogue at its deepest: a computer science idea (type theory) becoming a candidate foundation for mathematics itself, with the boundary between the two fields dissolving at the level of what a proof fundamentally is.

What This Perspective Changes

Seeing the relationship between computer science and mathematics changes how a practitioner understands both fields and their own work.

The first change is a correct understanding of the foundations. The practitioner who sees that the deepest foundations of computing are mathematical — that the theory of computation is mathematical logic, that algorithm analysis is applied mathematics, that the security of cryptography rests on number theory — understands their field’s foundations correctly, as mathematical rather than merely technical. This understanding makes the foundations more solid, because they are seen as theorems rather than conventions, and it makes the foundational chapters of this guide legible as the mathematics they are.

The second change is calibration about rigor and proof. The practitioner who understands the difference between the mathematical and the experimental cultures of computer science can apply the right standard to each kind of question. Some questions in computer science are mathematical and demand proof (does this algorithm always terminate? what is its worst-case complexity?); others are empirical and demand experiment (does this system perform well in practice? does this heuristic work on real data?). The practitioner who knows which kind of question they are facing applies the appropriate standard, rather than demanding proof where experiment is appropriate or accepting experiment where proof is required.

The third change is appreciation for the depth of the connection at the foundations. The practitioner who understands the Curry-Howard correspondence — that proofs and programs are the same kind of object — sees their work differently: writing a well-typed program is, in a precise sense, constructing a proof, and the type system is a logic. This is not a metaphor; it is a mathematical identity, and seeing it changes how one understands what programming is. The deepest theoretical results in computer science are at this boundary with mathematics, and the practitioner who appreciates the connection has access to a way of thinking about computation that the purely engineering view does not provide.

The fourth change is the recognition that the relationship is alive and consequential. The dialogue between the fields — proof assistants changing mathematical practice, type theory offering new foundations for mathematics, computation enabling experimental mathematics — is active research that bears on what both fields are becoming. The practitioner who sees this understands that the boundary between computer science and mathematics is not a settled border but an active frontier, where some of the most interesting work in both fields is happening.

Resources

Foundational and Bridging Texts

Knuth’s Concrete Mathematics: A Foundation for Computer Science (Graham, Knuth, Patashnik, 2nd ed., Addison-Wesley, 1994) is the bridge text par excellence: written by a computer scientist (with mathematicians) to teach the mathematics that computer science actually uses, in the style and with the orientation that computer science needs. It covers sums, recurrences, number theory, combinatorics, and generating functions with the constructive, computational orientation that distinguishes the computer science use of mathematics from the pure-mathematics treatment. It is the book that most directly embodies the relationship between the fields.

Knuth’s The Art of Computer Programming (multiple volumes, Addison-Wesley) is the monument to the mathematical analysis of algorithms — the work that established that algorithms could be analyzed with full mathematical rigor, and that demonstrated what the mathematical treatment of computer science looks like at its most thorough. It is a reference rather than a read-through, but its existence and character define the mathematical tradition within computer science.

For the philosophy of the relationship, the writings on the nature of computer science as a discipline — including the debates about whether it is a branch of mathematics, a science, or an engineering discipline — illuminate the difference dimension. Knuth’s essays (collected in Selected Papers on Computer Science and elsewhere) reflect on the relationship from within, by someone who embodies both the mathematical rigor and the computational orientation.

Resource Role Type
Graham, Knuth & Patashnik, Concrete Mathematics (2nd ed.) The bridge text; CS mathematics Depth
Knuth, The Art of Computer Programming Mathematical analysis of algorithms; the monument Reference
Knuth, Selected Papers on Computer Science Reflections on the relationship from within Auxiliary

The Dialogue: Proofs, Programs, and Foundations

For the Curry-Howard correspondence and the deep identity between proofs and programs, the type theory resources of §3.5 are the entry; the correspondence is where the two fields meet at the foundations. Wadler’s expository writing on Curry-Howard (“Propositions as Types,” free, also a widely-available talk) is the most accessible introduction to why the identity of proofs and programs is profound and what it means.

For proof assistants and formalized mathematics, the Lean theorem prover (free, leanprover.github.io) and its mathematical library (mathlib) are the most active site of the contemporary dialogue, where mathematicians are formalizing substantial mathematics. The Natural Number Game (free, a browser-based introduction to Lean through building up arithmetic) is the most accessible entry to what formalized mathematics feels like. The Homotopy Type Theory book (free at homotopytypetheory.org/book) is the foundational text of the univalent foundations program, demanding but representing the deepest current dialogue between the fields.

For experimental mathematics and the use of computation in mathematics, Borwein and Bailey’s Mathematics by Experiment: Plausible Reasoning in the 21st Century documents the practice of using computation to investigate mathematical questions.

Resource Role Type
Wadler, “Propositions as Types” (free) Curry-Howard, accessibly explained Depth
Lean + mathlib (free) The contemporary formalization dialogue Practice
Natural Number Game (free) Accessible entry to formalized math Practice
Homotopy Type Theory book (free) The deepest current foundations dialogue Depth
Milewski, Category Theory for Programmers (free; paid print optional) Category theory as programming-language structure Auxiliary
nLab (free) Research-level wiki for type theory, category theory, and foundations Reference
Borwein & Bailey, Mathematics by Experiment Computation in mathematical practice Practice

Traps

Trap Why it misleads Better response
“Computer science is just applied mathematics” The view that computer science is merely a branch of applied mathematics captures the debt but misses the difference: computer science has its own orientation (toward computation and construction), its own experimental culture, and its own questions (about systems, performance, and behavior in practice) that are not mathematical questions and cannot be answered by mathematical means alone. Reducing it to applied mathematics misunderstands what the field actually is. Hold both the debt and the difference. The foundations are mathematical and the debt is permanent; and computer science is a distinct discipline, part mathematical, part experimental, part engineering, with an orientation and a set of questions that are its own. It uses mathematics without being reducible to it.
“Computer science doesn’t need real mathematics” The opposite error, common among practitioners who work at the application level: the belief that the mathematics is academic and irrelevant to real work. This holds until the practitioner hits a problem — a performance question requiring complexity analysis, a correctness question requiring formal reasoning, a machine learning problem requiring the underlying mathematics — where the missing mathematics is exactly what is needed and its absence is disabling. Recognize that the mathematics is the foundation beneath the engineering, and that the depth at which one needs it varies by the work. Application-level work may need little; systems, algorithms, security, machine learning, and graphics need substantial mathematics. The foundations are an investment that pays off when the work reaches the depth at which they become load-bearing — which it does more often than the application-level view expects.
Mistaking the experimental culture for a lower standard Computer science’s experimental culture — building and measuring rather than proving — can look, from a pure-mathematics perspective, like a lower standard of rigor. This misreads it: many of computer science’s questions are empirical, not mathematical, and the experimental method is the appropriate one for them. The standard is not lower; it is appropriate to a different kind of question. Apply the standard appropriate to the kind of question. Mathematical questions (does this always terminate? what is the worst-case complexity?) demand proof; empirical questions (does this perform well in practice? does this heuristic work on real data?) demand sound experiment. The error is applying the wrong standard — demanding proof for an empirical question, or accepting weak experiment for a mathematical one — not the existence of the experimental culture.

中文

计算机科学诞生于数学，并且从未真正离开这个家，但二者之间的关系已经变得比“父母与子女”更复杂。数学给予了计算机科学基础——逻辑、计算理论、算法分析，以及一切建立其上的结构——这份债务巨大而永久。但计算机科学不是应用数学；二者思考方式的差异，和这份债务同样重要。而且，这种关系已经变成一种对话：计算机科学现在也在反过来影响数学，重塑数学家所做的事情，甚至重塑他们认为何为证明。二者关系有三个维度——计算机科学欠数学什么，尽管有这份债务二者为何仍然不同，以及它们现在如何相互影响——理解这三个维度，是理解任何一门学科相对于另一门学科位置的必要条件。

这种关系值得单独考察，而不是被吸收进那些使用数学的基础章节中，原因在于：两个领域的边界处，存在一些关于二者最深层的问题。计算机科学是数学的一个分支，还是一门使用数学的独立学科？数学证明与计算机程序之间是什么关系——如某些深刻结果所暗示的那样，它们是同一类对象，还是根本不同？当一个证明长到任何人类都无法完整检查，但计算机可以验证它时，它仍然是证明吗？这些问题不是空洞的；它们关系到每个领域是什么，应该如何实践，以及其结果意味着什么。只有站在边界上，这些问题才会显现出来，因此这个边界值得直接考察。

本节不是数学教程——计算机科学所使用的数学已经放在基础章节中（核心内容见 §2.2–§2.6，逻辑与计算理论见 §3.1–§3.3）。本节考察的是学科之间的关系：债务、差异和对话。它假定读者已经接触过这些数学，并追问这些数学与计算机科学之间到底是什么关系。

背景知识：离散数学（§2.2）、计算理论（§3.2）、复杂性（§3.3）、逻辑（§3.1）和类型论（§3.5）会让这种关系变得可读；这里的重点是这些领域如何连接，而不是再次呈现它们的内容。

这种关系：CS 欠数学什么，如何不同，又如何反哺

债务

计算机科学欠数学的债务，在字面意义上就是基础性的：计算的基础是数学的，而且这些基础往往在计算机存在之前，就由数学家奠定了。

计算理论——什么是可计算的定义、某些东西不可计算的证明、按困难程度对问题分类——是数学。它由 Gödel、Church、Turing 和 Kleene 在 1930 年代作为数理逻辑的一支发展出来，当时还没有用于运行他们所刻画计算的计算机。Turing 机器是为回答数学基础中的一个问题（Hilbert 的 Entscheidungsproblem，判定问题）而定义的数学抽象；它后来成为物理计算机的概念基础，是结果，而不是原本意图。lambda 演算，即 Church 的另一种形式化方式，同样是对数理逻辑的贡献，后来成为函数式编程和编程语言理论的基础。计算机科学最深的基础，是数理逻辑中的定理。

算法分析是数学：渐近记号、递推关系、概率分析、组合计数，这些决定一个算法需要多少时间和空间的工具都是数学技术，而算法分析这个领域就是应用数学的一支。密码学建立在数论之上——因数分解的困难性、有限域与椭圆曲线的结构——而这些数论曾经是为自身而研究的纯数学，早在它保障互联网安全之前就已存在。机器学习建立在线性代数、概率、优化和统计之上；数学对它来说不是附带的，而是构成性的。图形学建立在线性代数和光传输的微积分之上。整个领域中，这种模式反复出现：每个方向在工程之下的实质，都是数学。

这份债务并不只是历史性的。数学仍然是计算机科学最深结果被陈述和证明的语言，是新领域寻找工具时的来源，也是该领域理论部分用来要求自身的严谨标准。理论计算机科学家在某种意义上是一类数学家；复杂性理论论文中的证明，就是数学证明，也按照数学标准来要求。这份债务是持续而永久的：计算机科学不断从数学中汲取，二者关系并不是一个孩子长大后独立离家，而是一门学科的基础始终保持数学性质。

差异

尽管有这份债务，计算机科学并不是数学；二者思考方式上的差异真实而重要。这个差异不在于研究对象——二者高度重叠——而在于取向：每个领域试图做什么，重视什么，以及什么算作进展。

数学以真理和理解为取向：目标是证明定理，理解它们为什么为真，找到组织某类数学对象的结构和模式。数学家寻求证明，不只是为了知道某个东西为真，也是为了理解为什么为真；一个证明的价值，部分就在于它所提供的理解。计算机科学，即使在其理论部分中，也以计算和构造为取向：目标常常是构建某个东西，找到一个算法，让某个东西工作，而理论结果也经常服务于这一点。计算机科学家分析一个算法，是想知道它是否足够快；这和数学家追问“为什么”的问题不同，答案类型也不同。

这种取向带来了风格和价值上的差异。计算机科学比传统数学更关心构造性结果——也就是不仅证明某个东西存在，还提供构造它的方法——因为一个证明某个算法存在的非构造性证明，并不会给你那个算法。计算机科学以一种纯数学通常不具备的方式关心效率——不只是某件事能否完成，还要看它花费多少——因为当目标是实际计算时，成本就是问题本身。计算机科学也更能接受近似的、启发式的、概率性的、经验验证的结果，因为这些往往足以构建能工作的东西；而数学传统上更坚持精确和证明。两个领域共享技术，内容也有重叠，但计算机科学家和数学家是在用这些技术做不同的事情，而这种差异体现在他们认为怎样的结果令人满意。

差异在证明与实验的角色上最为尖锐。数学是一门证明学科：一个结果在被证明时才被确立；实验（计算例子、检查案例）可以提示结果，但不能确立结果。计算机科学则拥有相当重要的实验文化：系统会被构建和测量，算法会被实现和 benchmark，关于行为的假设会被经验检验，而这个领域的许多知识是通过实验而不是证明确立的。这不是缺陷——计算机科学的许多问题（这个系统在真实负载下表现好吗？这个启发式方法在真实输入上有效吗？）并不是可以被证明的那类问题，必须通过经验方式研究。但这也使计算机科学成为一种不同于数学的学科：部分是数学，部分是实验，部分是工程，而这种组合属于它自身，并不能还原为其中任何一部分。

对话

这种关系已经变成双向的：计算机科学现在也在反哺数学，而且正在重塑数学实践，甚至重塑数学基础。

最直接的馈赠，是计算作为数学工具。计算机让数学家能够探索、计算例子、测试猜想，并以手工不可能达到的规模发现模式。实验数学——使用计算以经验方式研究数学问题、生成猜想并为其收集证据——正是由计算机科学使其成为可能的一种持续增长的实践。有些著名结果是通过计算发现或验证的：四色定理在 1976 年被证明，其证明需要计算机检查成千上万个案例，无法由人类完整验证，这提出了一个问题：一个没有人能完全检查的证明，还是证明吗？这是计算机科学迫使数学面对的问题。

更深层的馈赠是概念性的：计算机科学贡献了一些思想和框架，改变了数学如何被实践和理解。证明助手——例如 Coq、Lean、Isabelle 这类用于形式化数学证明并由计算机检查的软件系统——已经从一种奇物成长为严肃工具，被用于验证那些过于复杂、无法让人类有信心完整检查的证明（例如四色定理、Feit-Thompson 定理的形式化验证，以及近期对前沿研究数学的形式化工作）。Lean 定理证明器吸引了一个数学家共同体，正在形式化大量数学；Fields Medalist Terence Tao 等人也已经把它用于研究级工作。这是计算机科学在改变数学实践：证明助手这一计算机科学产物，正在成为某些数学被完成和验证的方式之一。

最深的对话发生在基础层面，通过 Curry-Howard 对应及其后继发展展开。Curry-Howard 对应（§3.5）发现，证明和程序是同一类对象：一个命题的证明，就是对应类型的程序。它揭示了逻辑与计算之间的深刻同一性；这种同一性既属于两个领域，也不单独属于任何一方。它的现代发展——同伦类型论和单价基础计划（由数学家 Vladimir Voevodsky 发起，而他本人借鉴了来自计算机科学的类型论）——提出了一种基于类型论而非集合论的数学新基础。在这种基础中，计算机科学意义上的类型是首要概念，证明天生具有计算性并且可被检查。这是最深层的对话：一个计算机科学思想（类型论）成为数学自身基础的候选方案，而两个领域的边界在“证明本质上是什么”这一层面上开始溶解。

这种视角会改变什么

看清计算机科学与数学之间的关系，会改变实践者理解两个领域以及自己工作的方式。

第一个变化，是正确理解基础。一个实践者如果看见计算的最深基础是数学的——计算理论是数理逻辑，算法分析是应用数学，密码学安全建立在数论上——就会正确理解自己领域的基础：它们是数学基础，而不只是技术基础。这种理解会让基础更稳固，因为它们会被看成定理，而不是惯例；也会让本指南的基础章节变得可读，因为它们本来就是数学。

第二个变化，是对严谨性和证明的校准。一个理解计算机科学中数学文化与实验文化之差异的实践者，能够为不同问题使用正确标准。有些计算机科学问题是数学问题，需要证明（这个算法总会终止吗？它的最坏情况复杂度是什么？）；另一些问题是经验问题，需要实验（这个系统在实践中表现好吗？这个启发式方法在真实数据上有效吗？）。知道自己面对的是哪一类问题的实践者，会应用恰当标准，而不是在适合实验的问题上要求证明，或在需要证明的问题上接受实验。

第三个变化，是理解基础层面的深层连接。一个理解 Curry-Howard 对应的实践者——即证明和程序是同一类对象——会以不同方式看待自己的工作：写出一个良类型程序，在精确意义上就是构造一个证明，而类型系统就是一种逻辑。这不是隐喻；这是数学同一性。看见这一点，会改变人们对编程是什么的理解。计算机科学中最深的理论结果，就位于它与数学的这条边界上；理解这种连接的实践者，会获得一种纯工程视角无法提供的计算思维方式。

第四个变化，是认识到这种关系仍然活着，而且后果重大。两个领域之间的对话——证明助手改变数学实践，类型论为数学提供新基础，计算使实验数学成为可能——都是正在进行的研究，并且关系到两个领域正在变成什么。看见这一点的实践者会明白：计算机科学与数学之间的边界不是一条已经确定的国境线，而是一条活跃前沿，两个领域中一些最有意思的工作正在这里发生。

资源

基础性与桥梁性文本

Knuth 的 Concrete Mathematics: A Foundation for Computer Science（Graham、Knuth、Patashnik，第 2 版，Addison-Wesley，1994）是最典型的桥梁文本：它由一位计算机科学家（与数学家合作）写成，目的是以计算机科学所需要的风格和取向，教授计算机科学实际使用的数学。它覆盖求和、递推、数论、组合数学和生成函数，并带有区分 CS 使用数学方式与纯数学处理方式的构造性、计算性取向。这本书最直接地体现了两个领域之间的关系。

Knuth 的 The Art of Computer Programming（多卷本，Addison-Wesley）是算法数学分析的纪念碑式作品——它确立了算法可以以完整数学严谨性被分析，也展示了对计算机科学进行数学处理时最彻底的样子。它是参考书，而不是适合通读的书，但它的存在和风格定义了计算机科学内部的数学传统。

关于这种关系的哲学层面，讨论计算机科学作为一门学科之性质的著作——包括它究竟是数学分支、科学，还是工程学科的争论——照亮了“差异”这一维度。Knuth 的文章（收录于 Selected Papers on Computer Science 等文集）从内部反思这种关系；他本人正体现了数学严谨性与计算取向的结合。

资源 作用 类型
Graham, Knuth & Patashnik, Concrete Mathematics（第 2 版） 桥梁文本；CS 数学 深入
Knuth, The Art of Computer Programming 算法的数学分析；纪念碑式作品 参考
Knuth, Selected Papers on Computer Science 从内部反思这种关系 辅助

对话：证明、程序与基础

对于 Curry-Howard 对应，以及证明与程序之间的深层同一性，§3.5 中的类型论资源是入口；这个对应正是两个领域在基础层面相遇之处。Wadler 关于 Curry-Howard 的解释性写作 “Propositions as Types”（免费，也有广泛可获取的演讲）是理解为什么证明与程序的同一性如此深刻、以及它意味着什么的最可进入介绍。

对于证明助手和形式化数学，Lean theorem prover（免费，leanprover.github.io）及其数学库（mathlib）是当代对话最活跃的场所，数学家正在其中形式化大量实质性数学。Natural Number Game（免费，基于浏览器，通过逐步建立算术来介绍 Lean）是进入“形式化数学感觉如何”的最易入口。Homotopy Type Theory book（可在 homotopytypetheory.org/book 免费获取）是单价基础计划的基础性文本，要求很高，但代表了两个领域之间当前最深层的基础性对话。

对于实验数学，以及计算在数学实践中的使用，Borwein 和 Bailey 的 Mathematics by Experiment: Plausible Reasoning in the 21st Century 记录了使用计算研究数学问题的实践。

资源 作用 类型
Wadler, “Propositions as Types”（免费） 以可进入方式解释 Curry-Howard 深入
Lean + mathlib（免费） 当代形式化对话的核心场所 实践
Natural Number Game（免费） 进入形式化数学的可访问入口 实践
Homotopy Type Theory book（免费） 当前最深的基础性对话 深入
Milewski, Category Theory for Programmers（免费；纸质版可付费购买） 作为编程语言结构的范畴论 辅助
nLab（免费） 类型论、范畴论和基础研究级 wiki 参考
Borwein & Bailey, Mathematics by Experiment 数学实践中的计算 实践

陷阱

陷阱 为什么会误导 更好的回应
“计算机科学只是应用数学” 把计算机科学仅仅视为应用数学的一支，确实抓住了债务，却错过了差异：计算机科学有自己的取向（面向计算和构造），有自己的实验文化，也有自己的问题（关于系统、性能和实践中的行为），这些问题不是数学问题，也无法仅靠数学手段回答。把它还原为应用数学，会误解这个领域实际是什么。 同时保留债务与差异。基础是数学的，债务是永久的；但计算机科学是一门独立学科，部分是数学，部分是实验，部分是工程，拥有自身取向和自身问题。它使用数学，但不能被还原为数学。
“计算机科学不需要真正的数学” 这是相反错误，常见于在应用层工作的实践者：认为数学只是学术性的、与实际工作无关。这个看法会成立到实践者撞上某个问题为止——例如需要复杂度分析的性能问题，需要形式推理的正确性问题，或者需要底层数学的机器学习问题——此时缺失的数学恰好就是所需之物，而它的缺席会让人无法前进。 认识到数学是工程之下的基础，并且一个人需要数学的深度取决于其工作类型。应用层工作可能需要很少数学；系统、算法、安全、机器学习和图形学则需要大量数学。基础是一项投资，当工作达到它成为承重结构的深度时，它就会产生回报——而这种情况比应用层视角预期得更常发生。
把实验文化误认为更低标准 从纯数学视角看，计算机科学的实验文化——构建和测量，而不是证明——可能像是一种较低的严谨标准。这是误读：计算机科学的许多问题是经验问题，而不是数学问题，实验方法正是适合它们的方法。标准不是更低，而是适合另一类问题。 为问题类型使用合适标准。数学问题（它是否总会终止？最坏情况复杂度是什么？）需要证明；经验问题（它在实践中表现好吗？这个启发式方法在真实数据上有效吗？）需要可靠实验。错误不在于实验文化存在，而在于用错标准——对经验问题要求证明，或对数学问题接受薄弱实验。