你以为数学就是画几何图、会算术、能数数？幼稚了

数学追求严谨与直觉的平衡，历史上数学家们为形式化而努力，催生了新领域。

Lean程序的出现增强了数学证明的严谨性，但可能限制了创造力与多样性。

数学家需在严谨与直觉之间寻求新的平衡。

古希腊的欧几里得提出了用逻辑推理建立数学真理的想法，但早期证明常有潜规则和直觉的影响。

数学家们追求绝对真理，开始了形式化的努力，确保每一步推理都严谨。

形式化的浪潮帮助数学家发现不同领域之间的联系，开拓了新天地。

大胆的想法和实验直觉是数学进展的关键，但形式化可能会抑制创造力。

微积分的严谨化是数学史上的里程碑，牛顿和莱布尼茨的工作虽然不够形式化，但推动了数学的发展。

19世纪初，数学家们开始对无穷和曲线进行严谨的形式化定义，催生了分析学和集合论。

布尔巴基社团追求极致的形式化，影响了全球数学风格，但也导致了数学的抽象化和难懂。

Lean程序作为证明助手，提供了标准化的数学积木，但也可能导致数学研究的同质化。

Lean的使用可能会限制数学家对问题的选择，导致研究者倾向于选择易于形式化的课题。

数学的严谨性与直觉性之间的平衡仍然是一个重要的课题，未来可能会出现多种证明助手以适应不同的数学文化和风格。