如何评价 GPT-5.6 Sol 打破了大素数间隙保持八年的世界纪录？

8 月下旬，Jared Duker Lichtman称GPT-5.6 Sol 给出了一篇关于大素数间隙的新证明，将 2018 年 Ford、Green、Konyagin、Maynard、Tao 的已知最佳下界 G(X)\gg \frac{\log X\,\log_2X\,\log_4X}{\log_3X} 改进为 G(X)\gg \frac{\log X\,\log_2X}{\log_4X}. 两者之比为 \frac{\log_3X}{(\log_4X)^2}\to\infty, 这个方向有很长的历史。Westzynthius 在 1931 年证明素数间隙相对于平均间距可以任意大，Erdős 和 Rankin 在 1930 年代继续推进。Erdős 后来提出的 Problem #4 长期悬而未决，直到 2014 年左右被 James Maynard 和 Ford–Green–Konyagin–Tao 两组独立解决，相关论文后来发表在 Annals of Mathematics。2018 年，五人合作又把定量下界推进到上述 FGKMT 尺度。 这次的新结果进一步改进了 Erdős #4这条经典研究主线上的已知最佳渐近下界。 Boris Alexeev 随后已经将新结果形式化到 Lean。 想请教解析数论方向的老师和研究者几个问题： 这个新的 tilted residue-class construction 相比 FGKMT 2018 的核心技术创新到底在哪里？ 从数学史角度看，从 \frac{\log X\log_2X\log_4X}{\log_3X} 推进到 \frac{\log X\log_2X}{\log_4X} 属于什么级别的进展？目前公开的 Lean 形式化能在多大程度上消除对证明正确性的疑问？还有哪些地方需要解析数论专家人工审阅？这个结果距离通常认为的大素数间隙真实尺度，例如 Cramér 型的如果最后确认无误，这是否可以视为 AI 首次在一条经典数学研究主线上，对由顶级数学家保持多年的 best-known asymptotic bound 作出实质改进？