GPT-5.6 Pro 参与 Bondy minimum-degree longest-cycle conjecture proof candidate，Lean 检查精确 endpoint

Lech Mazur 发布 Bondy 1980 minimum-degree longest-cycle conjecture 的 proof candidate。GPT-5.6 Pro 参与 computation、proof strategy、gap discovery、formalization 与 exposition；一个 204-module、约 10 万行的 first-party Lean cone 检查精确 theorem `Bondy.bondy_longest_cycle`，无 unfinished proof。ProofAtlas 同时明确：paper-to-formal-statement alignment、specialist peer review、unrelated replication 与 historical priority 仍未完成。