Lean v4.17 发布，包含 319 项更改：

• 新增 168 个功能，如：

  • [#5145] 分离内核和细化器使用的环境，为跟踪异步细化声明奠定基础。
  • [#6261] 添加 foo.fun_cases 定理，根据 foo 的分支结构拆分目标。
  • [#6355] 可定义可能非终止函数并进行等式推理。
  • [#6368] 实现并行执行内核检查和细化。
  • [#6427] 添加 --src-deps Lean CLI 选项。
  • [#6486] 修改 induction/cases 语法。
  • 等。

• 修复 57 个问题，如：

  • [#6565] 修复 rintro 和 intro 战术引入请求数量的绑定器时的位置错误。
  • [#6566]、[#6567] 为 grind 中的启发式实例化添加支持删除 [grind] 属性。
  • 等。
• 进行 12 项重构更改，13 项文档改进和 56 项杂项工作。

• 还包含众多关于 grind 战术的改进，如：

  • 支持各种操作，如加法、乘法、移位、比较等的常量折叠和重写。
  • 增强模式选择和匹配功能，包括处理重叠模式、处理条件方程等。
  • 改进错误消息、诊断信息和搜索过程。
  • 支持更多类型和结构，如 UIntX、USize、Offset 等。
  • 增加配置选项和属性，以更好地控制 grind 的行为。

• 此外，还对其他部分进行了更新，如：

  • 完成 List、Array、Vector 等数据结构相关的定理和引理的对齐和补充。
  • 对 BitVec 相关操作和定理进行了大量的添加和改进。
  • 对 HashMap、DHashMap 等数据结构的操作和定理进行了优化。
  • 对 Std.Time、Std.Net 等标准库部分进行了相关工作。