AI agents 为 Bugeaud Problem 10.61 建立可检验 certificate 框架，并在两个二次 Pisot 情形完成 Lean 证明

Ralf Stephan 发布针对 Bugeaud Problem 10.61 的 Lean 4 / Mathlib development。公开记录明确写明数学与 Lean 文本由 agents 产生：Fable-5 agent 撰写数学笔记，Opus-5 agent 完成形式化，作者负责选题、逐轮引导与筛选结果。项目把问题转化为 symbolic-dynamics、pressure 与 covering certificates，并在 α=2+√5 和 α=2+√3 两个 quadratic Pisot 情形真正推出非均匀分布结论；一般问题及超出该 covering range 的 quadratic cases 仍保持开放。