数学小站

Lean 是一个交互式定理证明器，也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。

Lean 是一个交互式定理证明器，也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。

华罗庚诞辰 113 周年，纪念华老，以自我勉励。

原文链接：数独探秘 | 藏在九宫格下的数学天地。

这是 Programming For Math 系列，探索编程结合数学的思路。本篇介绍数独的数学背景，以及用 C 语言实现数独的过程。