2026-07-20

新确定性并行算法证明二分图完美匹配属于NC，解决长期开放问题，是计算复杂性理论的重大进展。 在 Mathlib 中形式化了交换代数中的上升性质（Going Up），证明其与素谱特殊化映射提升等价，并推广了理想链的存在性定理。

Bipartite Perfect Matching in Deterministic NC 85

• Tags: 理论计算机 算法 组合优化

• Source: Computational Complexity Blog | 阅读原文

[摘要]
新确定性并行算法证明二分图完美匹配属于NC，解决长期开放问题，是计算复杂性理论的重大进展。

---

master-2026-07-19: feat(RingTheory/Ideal): add Algebra.HasGoingUp (#40911) 68

• Tags: 交换代数 形式化数学 整扩张

• Source: GitHub Release - mathlib4 | 阅读原文

[摘要]
在 Mathlib 中形式化了交换代数中的上升性质（Going Up），证明其与素谱特殊化映射提升等价，并推广了理想链的存在性定理。

---