探索 AI 辅助数学研究、算法分析与 Lean 形式化证明。
从计算实验和猜想到数学论证、机器检查与可复验的成果归档，保留每一步的证据和开放问题。
| 项目 | 内容 |
|---|---|
| 3SUM | 算法指数研究、解析证书与成果归档 |
| Average Sensitivity | 多项式阈值函数平均敏感度与 Lean 证明 |
| Prove2Me Workspace | 多课题研究、共享 Lean/Mathlib 环境与状态文档 |
| Sharp diagonal Hlawka | p ≥ 21 的计算机辅助证明预印本；完整 Lean / 平台证明通过，零开放依赖；正式 mission / campaign 认证 21 |
| Angel–Devil | 标准 Devil 下的整数力量完整分类：1 阶必败、p≥2 必胜；Lean 与平台验证完成，开放叶子 0 · 统一 mission：分类 Proved，4/4 里程碑完成 |
- 数论与分析：无理性、特殊常数、素数与多项式。
- 组合数学与概率：幻方、离散结构与概率模型。
- 算法与复杂度：3SUM、近似算法与平均敏感度。
- 形式化数学：Lean、Mathlib、证明依赖与可复现验证。
各课题的进展和验证范围以对应仓库中的证据为准。实验观察、数学论证、形式化验证与论文发表分别记录。
由 Anchen0823 维护。
