走 Darmon–Diamond–Taylor 路线，非他推进的 Khare–Taylor 现代路线；对 n 的限制靠既有正则素数结果兜底
数学上不增加新内容，但作为自动形式化的可能性信号意义重大
他仍继续 EPSRC 项目：为 Lean 数学库贡献现代数论对象、做人类可探索的动态文档
金句
What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end ... in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly.