详细内容或原文请订阅后点击阅览
程序员精益简介
数学的语法和语义这篇文章《程序员精益简介》首先出现在《走向数据科学》上。
来源:走向数据科学打样助手简介
转向了数据科学，我每天都在研究机器学习算法。我对它们明显的魔力和它们背后的数学着迷。打开任何机器学习库，你都会发现涉及矩阵分解、卷积、高斯曲线等的数学技巧。反过来，这些又建立在更基本的公理和规则之上，例如函数应用和逻辑。
在学习这些原语的过程中，我收集了整整书架的数学书籍，其中许多现在都已落满灰尘。我还就读于开放大学，在那里我通过 Zoom 参加课程，学习语法和公理，然后如何将它们结合起来构建定理。
这个话题很有趣：公理就像游戏棋子和棋盘上的合法走法，而定理则是合法的游戏，有些比其他更有趣。证明定理意味着将游戏玩法展开到足以让玩家相信它是可以实现的，或者通过指出不可能来反驳它。例如：“两个主教都在白色方格上，主教永远不能切换到不同颜色的方格上。”
但在实践层面上，这些课程很乏味。我得到了 PDF 供我手工解答，然后在线提交我的作品的扫描件。当我用铅笔在纸上涂鸦、努力完成课程作业时，我有了两个见解：
我的想法并不新鲜。第一个想法称为库里-霍华德对应关系，如下所述。后者是 Lean 及其 IDE 扩展（通常是 VS Code 扩展）等证明助手的目标。
交互式证明助手与自动定理证明者
库里-霍华德通信
(P → Q → R) → (P ∧ Q → R)
通用且简化（playground）：