写作方法2018blogs.scientificamerican.com
Leslie Lamport 教数学家如何写证明
Leslie Lamport Tells Mathematicians How to Write Proofs (2014)
导读
这篇文章介绍计算机科学家 Leslie Lamport 的主张：数学家写证明应当像写代码一样严格——每一行都给出依据，并按假设层级组织成结构化证明。值得写作者读，因为它把"写多细才算够"这个所有写作都会遇到的问题，放在数学证明这一极端场景下讨论清楚了。
可以直接用的写作要点
- 01
每一行论断都注明依据（引用的定义、定理或前提假设），能逼自己发现推理中偷偷跳过的那一步。
- 02
按假设的层级组织长论证：外层先讲主干，读者需要时再进入子层看细节，这样不同水平的读者都能各取所需。
- 03
面向同行写作时，省略"对懂的人来说显然"的细节是一种专业文体，就像散文不把每件事都掰开揉碎讲给读者听。
- 04
严格完备的写法适合查错和教学，叙述式写法信息密度更高、更适合传达直觉，应按写作目的在两者间切换。
HN 评论精选
严格证明适合查错和机器验证，但论文交流用叙述式证明效率更高。
Lamport 主张证明要更严格：每一行都要有理由，并按假设前提的层级来排列行。他也是形式化证明检查器 TLA+ 的作者。完全给出理由的证明常用于几何和抽象代数的教学，机器验证的证明也需要它。在这些场景之外，我同意 Lamport 说的它能帮你抓错，但我自己不会那样写，因为太繁琐了。论文里用于交流时，叙述式证明传达想法和直觉的带宽要高得多。
allenz查看英文原文
Lamport advocates for more rigorous proofs with a justification for every line, and lines arranged in a hierarchy based on assumption contexts. He is also the author of TLA+, a formal proof checker: https://en.wikipedia.org/wiki/TLA%2B Fully-justified proofs are frequently used to teach geometry and abstract algebra, and are also needed for machine-checked proofs. Outside these contexts, I agree with Lamport that they are useful to catch mistakes, but I wouldn't write them myself because they are incredibly tedious. For communication in papers, narrative proofs can convey ideas and intuition at a much higher bandwidth.
省略显而易见的细节是面向同行的专业文体，而非偷懒。
数学家写给同行看时，并不追求最大程度的显式证明，很多细节因为对懂行的读者来说显而易见而被省略。省略繁琐内容是专业风格问题，就像把普通文章收紧，不要拿每个细节去砸读者的头。（我的傅里叶分析课老师在答疑时看到我那些过于详尽的证明会微微皱眉，但他知道我是计算机科学家，就礼貌地什么也没说，因为他知道说了也没用 ;-)
aoki查看英文原文
mathematicians writing for peers don’t aim for the maximally explicit proof. details are frequently left out as obvious to the knowledgeable reader. leaving out tedious matter is a matter of professional style, like tightening regular prose so it doesn’t club the reader over the head with every detail. (my instructor in Fourier analysis would subtly grimace at my very explicit proofs in office hours, but he knew i was a computer scientist so he politely said nothing because he knew it would do no good ;-)
Dijkstra 的证明格式把步骤用蕴含/等价关系串联并记录每步有效性，可读性极高。
Dijkstra 也常在他的 EWD 笔记里批评传统数学家的马虎。他的证明格式可读性极强，每个证明都是一个完整、可操作推演的数学对象，各步骤用蕴含、推论或等价关系串起来，并且每一步的有效性都有据可查。
User23查看英文原文
Dijkstra also challenged the sloppiness of traditional mathematicians frequently in his EWDs. His proof format is extremely readable, and each proof is a complete manipulable mathematical object, with the steps tied together by implication, consequence, or equivalence and the validity of the step documented.
附上 Lamport 层级式证明的原始说明文档。
这里是 Lamport 对层级式证明的说明：https://lamport.azurewebsites.net/pubs/proof.pdf
lixtra查看英文原文
Here is the description of hierarchical proofs: https://lamport.azurewebsites.net/pubs/proof.pdf
同类还值得读
被低估的工程技能：把文章写好
Undervalued Engineering Skills: Writing Well
这篇文章讨论为什么“写得好”是被低估的工程能力，以及它如何在团队协作、系统设计和职业发展中持续带来回报。
写作方法2019 · 1,109 分 · 371 评4 条写作要点编辑精选每行只写一句话：让写作和修改都更轻松的排版法
Writing one sentence per line
这是 Derek Sivers 的一篇短文，主张写作时每行只放一个句子，而不是按段落排版。
写作方法2022 · 849 分 · 297 评4 条写作要点编辑精选书面沟通是远程工作的超级能力
Written communication is remote work super power
这篇文章讨论远程工作中书面沟通的价值，评论区则补充了异步与同步沟通的适用场景，并提醒读者：备忘录、结论先行、结构化命令格式等书面沟通传统早已有之。
写作方法2020 · 831 分 · 190 评4 条写作要点编辑精选如何写出有用的文字
How to Write Usefully
保罗·格雷厄姆在这篇文章里给"有用的写作"下了一个可操作的公式：有用≈重要×新颖×正确×清楚，任一项为零，整篇文章就等于零；他还主张敢下确定判断、删掉让自己心虚的句子。
写作方法2020 · 821 分 · 285 评4 条写作要点编辑精选如何写得更清楚、想得更清楚，并学会复杂材料（PDF）
How to write more clearly, think more clearly, and learn complex material [pdf]
这份 PDF 讨论如何把文章写清楚、把思路理清楚，并用写作来学习复杂材料。
写作方法2022 · 779 分 · 153 评4 条写作要点编辑精选