技术写作与文档2015blogs.scientificamerican.com
一位计算机科学家教数学家如何写证明
A Computer Scientist Tells Mathematicians How to Write Proofs
导读
这篇文章是计算机科学家 Leslie Lamport 向数学家分享写证明的建议，但评论者指出标题制造了计算机科学与数学的虚假二分，并深入讨论了数学证明与计算机科学证明在目的和受众上的差异。对写作者而言，它提醒我们写作目的和受众决定细节程度：面向人类理解可省略细节、依赖共识，而面向实际系统验证则需严谨详尽；同时，明确前提和步骤引用能帮助发现错误并简化结构。
可以直接用的写作要点
- 01
明确写作目的和受众：是为了传达洞察还是提供无错误的验证，这决定你省略多少细节、依赖多少共识。
- 02
面向人类读者时，可以依赖共享背景知识、省略可自行验证的细节，以优先传达核心洞察。
- 03
在论证中每一步明确引用前提和依据，有助于发现逻辑错误，并促使你重构简化整体结构。
- 04
标题和表述要准确，避免制造虚假对立或误导读者对领域的认知。
HN 评论精选
标题制造虚假二分，误导读者；CS与数学本质相通。
作为数学出身、在CS理论读研的人，我认为标题制造了CS与数学的虚假二分，实际是数学家之间的对话。Lamport的领域本质是数学性的。标题误导，但很高兴这些大家在思考数学教育。
kiyoto查看英文原文
As a math major who went to grad school in CS theory, I find the article's title vexing. It projects a faux dichotomy of computer scientists v. mathematicians when, in reality, it's mathematicians v. mathematicians. Many areas of computer science, at least the areas in which Leslie Lamport is best known, is a strongly mathematical discipline inspired by models of computing. Dr. Lamport probably considers himself as a "computer scientist", but I bet it is really far from what many laypeople (even the HN crowd) imagine to be computer scientists. Another issue is, mathematicians have as much to do with mathematical pedagogy in secondary education as computer scientists have to do with science experiments in high school. Again, the title is really misleading in this regard. Anyway, I am glad that a great mind like Leslie Lamport and David Mumford (definitely a mathematician) are thinking hard about how to make math education better.
写作目的决定细节程度：数学证明为人类洞察可省略细节，CS证明为系统安全需详尽无遗。
数学证明旨在向人类传达洞察，依赖潜在知识、省略细节是有效沟通，允许偶尔错误，因为数学整体容错。而Lamport的CS领域研究分布式协议用于实际系统，证明是为了系统安全，因此需要无错误的长篇证明。两者目的不同。
j2kun查看英文原文
I agree with the concerns on the false dichotomy between theoretical computer science and mathematics, but from the mathematician's perspective I think there's another issue not being discussed due to the typical CS obsession over automated proof systems. Mathematics is a social subject, invented by humans largely for their own amusement. The goal of a mathematical proof is to communicate insight to other humans. Of course the point is also to be correct, but somehow communicating insight takes priority. Relying on large bodies of latent knowledge, and omitting details, is an effective way to do that. Allowing for occasional mistakes is okay, because mathematics as a whole is fault tolerant (or at least, history gives evidence to that claim). Lamport's field is a bit different, because there they study distributed protocols with the intent of creating value in the real world. So when they prove a theorem, they're not just proving a theorem to gain understanding about something, they're proving a theorem so they can improve the security or fault-tolerance (or whatever else) of some real system. Writing down a 200+ page TLA proof is measurably worth the investment because the users of their work (applied computer scientists and engineers) want error-free theorems and a clean CS literature much more than they want insight. For mathematicians communicating to other mathematicians, a two-paragraph argument that is convincing and omits the details (that one can verify on their own) is much more valuable. I'm not trying to make a value judgement either way, just trying to explain the culture of math proofs and why I think something like TLA+ will never catch on among mainstream mathematicians. You might say it's mathematicians defending their job security, but it's also simply that mathematicians like exploring and inventing and hearing creative proofs and perspectives. Deferring things to computers removes the a-ha moment. [Edit] And the idea that somehow high school students and undergraduates will magically start reading and understanding proofs because we write them using TLA+ is a joke.
写作中明确前提和步骤引用能发现错误，并促使重构简化。
文章例子有错（x^2+10x=39有两个解）。这正说明每一步引用前提能发现错误。写代码经验表明，这也能让证明更美观，因为发现某步依赖大量引用会促使重构简化证明。
mitko查看英文原文
Pretty good read, but the OCD in me could avoid pointing out that the example they give has a wrong solution: x2+10x=39. Find x2. This actually has two solutions for x: 3 and -13, so x^2 is 9 or 169. It is probably a good example of how referring to preconditions at every step of the proof would help catch errors. From my experience writing code, I'd also argue that this would also make proofs more beautiful, because discovering that some steps require a lot of previous references might prompt the mathematician to restructure/refactor the proof to make it simpler to write, thus making it simpler overall.
同类还值得读
编写更好文档的框架
A Framework for Writing Better Documentation
这是 Divio 的文档写作框架，把技术文档按「读者的目标」分成四类：教程（学习导向）、操作指南（问题导向）、参考（信息导向）、解释（理解导向）。
技术写作与文档2021 · 637 分 · 76 评4 条写作要点编辑精选写好一份设计文档
Writing a good design document
这篇 HN 帖子标题为《Writing a good design document》，主题是如何写好一份设计文档；对写作者来说，它值得作为技术写作和结构化说明文的参照。
技术写作与文档2025 · 581 分 · 147 评3 条写作要点编辑精选技术写作课程
Technical Writing Courses
这是 Google 官方免费技术写作课程（两门），讲受众定义、主动语态、短句、文档结构等基础方法。
技术写作与文档2020 · 571 分 · 73 评4 条写作要点编辑精选写出更好的错误信息
Write better error messages
这篇帖子讨论如何写出更好的错误信息，评论补充了开发者场景下的具体做法和真实反面案例。
技术写作与文档2022 · 566 分 · 253 评4 条写作要点编辑精选写一本技术书的经济账
The Economics of Writing a Technical Book
一位技术书作者拆解写书的真实经济账：版税收入往往远低于投入的时间成本。
技术写作与文档2018 · 519 分 · 149 评4 条写作要点编辑精选