想要支持的证明大概是这样的 https://github.com/AxiomMath/IMO2026/blob/main/IMO2026/Q2/solution.lean 但是要做可视化 当前只有自然数的证明，效果在 https://bombless.github.io/prover-typescript/ 我目前还在免费的 luna 上手工 loop 推进，还没提交

  • 情报分类：技术学习与提效
  • 分类依据：内容涉及技术、AI、软件工具或工程实践
  • 信息来源：服务器 / V2EX
  • 发布时间：2026/9/18 20:10:28