Conan Xu

AI4Math · 优化算法 · 形式化数学

我关注 AI4Math、优化算法和形式化数学，也开发帮助研究与学习的工具。

我的研究与实践围绕一个朴素的问题展开：如何把一个数学想法，逐步变成可以理解、计算与检验的结果？我研究 ADMM 迭代的收敛性与反例，用 Lean 4 表达优化算法的假设和证明，并探索 AI 参与数学研究的方式。

这里也有一个博客，记录推导、项目实践，以及学习过程中逐渐想明白的事。

精选研究

2026

Kenan Xu, Xiangfeng Wang · arXiv preprint

当第三个约束块为单位阵时，直接三块 ADMM 仍可能不收敛。通过周期轨道研究这一结构的边界，并探索 AI 辅助数学发现的过程。

Lean 4

形式化数学 · 开源项目

用 Lean 4 形式化自适应 ADMM 的收敛性分析，把算法、参数策略与数学假设之间的关系写清楚。

围绕教材阅读的学习工作台，把教材、提问、讲解与学习资料放在一起。