1/ AxiomProver 解決了 Fel 關於數值半群合衝的未解猜想，並在無需任何人工幹預的情況下，自主地用 Lean 語言生成了形式化證明。 這是人工智慧系統首次解決理論建構數學中尚未解決的研究難題，並實現了自我驗證。