数学

余弦相似度 (Cosine Similarity) 是一种衡量两个非零向量之间方向性的度量方法。它通过计算两个向量在多维空间中夹角的余弦值来评估它们的相似程度。当两个向量的方向越接近，它们的夹角越小，余弦值越大，表示它们越相似；反之，当两个向量方向越垂直，夹角越大，余弦值越小，表示它们相似度越低。余弦相似度广泛应用于文本挖掘、信息检索、推荐系统等领域，尤其适用于处理高维数据，并且对数据维度上的量级差异不敏感。 核心思想：余弦相似度忽略了向量的长度（大小），只关注向量方向上的差异。它将向量间的相似性转化为其夹角的余弦值，夹角越小，方向越一致，相似度越高。这使得它在处理文本频率等只关注词语相对重要性而非绝对数量的场景中表现出色。 一、为什么需要余弦相似度？在许多数据分析和机器学习任务中，我们需要量化两个数据对象之间的相似性。常见的方法是计算它们之间的距离，例如欧几里得距离 (Euclidean Distance)。然而，欧几里得距离在某些场景下存在局限性： 对向量长度敏感：欧几里得距离会受到向量绝对大小的影响。如果两个向量的方向一致，但其中一个向量的模（长度）非常大，欧几里...

三角函数 (Trigonometric Functions) 是一类在数学、物理、工程和计算机科学等领域具有广泛应用的基本函数。它们最初定义为直角三角形中角与边长之间的比值，随后通过单位圆被推广到任意实数和复数。三角函数的核心在于描述周期性现象和几何关系，是高等数学、微积分、傅里叶分析等理论的基石。 核心思想：三角函数通过将角度与长度比值或单位圆上点的坐标关联起来，实现对周期性变化和旋转运动的数学描述。它们揭示了圆形运动的内在规律，并成为分析振动、波、交流电等周期性现象不可或缺的工具。 一、三角函数的定义三角函数的定义有两种主要方式：基于直角三角形和基于单位圆。 1.1 基于直角三角形的定义对于一个直角三角形，其一个锐角 $\theta$ 的三角函数定义如下： 假设直角三角形的斜边为 $r$，与角 $\theta$ 相邻的直角边为 $x$（邻边），与角 $\theta$ 相对的直角边为 $y$（对边）。 正弦 (Sine, 简称 $\sin$)：对边与斜边的比值。$$ \sin \theta = \frac{\text{对边}}{\text{斜边}} ...

Lean 语言 是一种函数式编程语言，同时也是一个交互式定理证明助手 (Interactive Theorem Prover)。它由微软研究院开发，核心思想是基于依赖类型理论 (Dependent Type Theory) 构建一个强大的系统，既可以用于形式化验证（Formal Verification）数学定理和软件正确性，也可以作为一种通用编程语言。Lean 的目标是让数学家和计算机科学家能够以一种严谨、可验证的方式表达和证明复杂的概念。 核心思想： 函数式编程：所有计算都是通过函数来完成，强调不可变性。 依赖类型理论：类型可以依赖于值，使得可以在类型系统中直接表达数学命题和证明。 交互式证明：用户与系统交互，逐步构建证明，系统提供反馈和自动化推理工具。 形式化验证：通过严格的数学和逻辑推理，确保软件或数学定理的绝对正确性。 可执行性：理论上，Lean 中定义的数学对象和证明过程也可以被编译成高性能的代码执行。 一、为什么需要 Lean 语言？—— 形式化验证的崛起在数学和计算机科学领域，对精确性和可靠性的需求从未停止。传统的数学证明虽然严谨，但仍可能因人为错误...