Huang–Jiang–Oblomkov conjecture 获全一般性证明，并由 AxiomProver 在 Lean 中形式化核心有限恒等式

Huang、Lau 与 Ono 证明 Huang–Jiang–Oblomkov conjecture 对所有互素 1<a<b 的 torus-knot singularity X^a=Y^b 成立。主结果是一个更强的 finite identity，把 rank-N HJO sum 与有界 balanced cylindric partitions 的生成函数联系起来，取 N→∞ 得到原猜想。论文同时说明，AxiomProver 已在 Lean 中形式化该 finite identity 与 HJO conjecture，但形式化明确以两个已有文献结果作为条件输入。