What's new by TerryTao
·
一个验证估计的工具，II：灵活的证明助手
💡
原文英文，约1500词，阅读约需6分钟。
📝
内容提要
我更新了一个自动验证工具，使其成为灵活的证明助手，支持符号代数和交互式证明。用户可以输入高层策略，助手会执行计算，并支持渐近估计，计划进一步增强功能。
🎯
关键要点
- 更新了一个自动验证工具，使其成为灵活的证明助手，支持符号代数和交互式证明。
- 工具经历了两次重大改造，首次变为基础证明助手，第二次变为更灵活的证明助手。
- 当前版本的证明助手支持半自动交互式证明，用户提供高层策略，助手执行计算。
- 证明助手在Python的交互模式下工作，用户可以逐步输入命令。
- 工具支持渐近估计，能够实现非标准分析的概念。
- 当前的挑战是处理“max”类型的表达式，计划开发更强大的LogLinarith()版本。
- 未来计划开发用于估计符号函数的函数空间范数的工具，创建新的策略和引理。
- 欢迎对证明助手提出建议或贡献新特性，扩展其功能。
❓
延伸问答
这个证明助手的主要功能是什么？
这个证明助手支持符号代数和交互式证明，用户可以输入高层策略，助手执行计算。
证明助手是如何工作的？
用户在Python的交互模式下逐步输入命令，助手根据用户提供的策略执行计算，直到完成证明。
当前版本的证明助手有哪些新特性？
当前版本支持半自动交互式证明，并能够处理渐近估计和非标准分析的概念。
未来对证明助手有哪些计划？
未来计划开发更强大的LogLinarith()版本，并创建用于估计符号函数的函数空间范数的工具。
证明助手如何处理“max”类型的表达式？
目前，LogLinarith()对“max”类型的表达式处理不佳，计划开发更强版本以改进此功能。
用户如何参与到证明助手的开发中？
用户可以提出建议或贡献新特性，扩展证明助手的功能。
➡️
