descent

Descent 是一个用 Lean 4 编写的软件项目，为遗传理论提供形式化数学框架。其主要关注点是多基因评分（PGS）的可移植性，探讨关于其在不同人群中准确性与局限性的三个核心问题。 该仓库在 `OpenQuestions.lean` 中包含了严格的证明，对个体损失信息与噪声进行了分类。这些证明确立了在固定二阶矩与遗传输入下的精确可达范围，刻画了有限的演化或报告闭包，并定义了度量排序与决策代价的逆命题。理论领域包括用于信息定理的任意平方可积损失，以及用于精确范围的显式有限模型类。此外，高斯损失噪声由高斯测度导出。 `CheckThreeQuestions.lean` 中提供了合并的公理审计。关于多基因评分准确性的人口统计学预测的详细结果与限制，用户可参阅 `UNIVERSAL_PORTABILITY.md` 文档。 ### 构建 要构建该项目，请运行以下命令： ```sh lake exe cache get lake build Descent ValidationShared ``` ### 贡献 欢迎贡献。但适用严格规范： - 模拟绝不能用于拟合模型；它们仅用于验证已有的推导。 - 仅允许三条公理：`propext`、`Classical.choice` 和 `Quot.sound`。 ### 许可证 该项目采用 Apache-2.0 许可证。