新未名空间

有几个定理是关于机器学习的，就是机器能学到什么，什么不可能学到。最初有用形式语言理论表述的，
https://en.wikipedia.org/wiki/E._Mark_Gold
https://en.wikipedia.org/wiki/Language_ ... _the_limit
后来有所谓VC维数， https://en.wikipedia.org/wiki/Vapnik%E2 ... _dimension
​
​机器数学证明是另外一个问题，就是靠人的智能编程实现的机器证明。先说个有关而不不是数学定理机器证明的有Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry%E2% ... espondence
再说数学定理机器证明的几个结果：数理逻辑里的量词消去法和与之相关的Tarski–Seidenberg theorem（https://en.wikipedia.org/wiki/Tarski%E2 ... rg_theorem），还有源自代数几何的希尔伯特零点定理的Buchberger算法（https://en.wikipedia.org/wiki/Buchberger%27s_algorithm）。这些有很多已经超出了机器可学习的上限。但是是机器能证明的。把这些嵌入AI里面，能扩展DNN机器证明的能力，可这些不是机器学到的。嵌入DNN，比如设计接口以解决DNN和形式化的机器证明的交互问题，即自然语言和所嵌入机器正证明所用形式化语言（数理逻辑表达式或程序语言）的互译问题。
​
数学定理的机器证明和机器可学得（learnability）本不是一回事。机器可学得（learnability）的数学定理的证明最好的结果是机器可学得（learnability）的语言的子集（证明等价于语法分析）。所以证明如果超出了机器可学得（learnability），即不可能学得，那么就只能嵌入，即从外界引入，或者搜索匹配。

​与机器证明，直觉逻辑/构造逻辑，Curry-Howard对应有关的或者进一步的发展的一个纲领是univalent foundations https://www.ias.edu/ideas/2014/voevodsky-origins
https://www.ias.edu/math/sp/univalent/goals
https://www.ias.edu/idea-tags/univalent-foundations
Fields奖得主Vladimir Voevodsky 开创或者倡议的。
与univalent fiundation相关的计算项目：https://ncatlab.org/nlab/show/univalent ... athematics

太杂，你就直接说一个机器能证的，一个不能，一个也许能的例子

猜测这个版面上的常客差不多都不明白这些是啥。

现在已经可以用深度学习证明数学定理了，YouTube上有

forecasting 写了： 2024年 10月 15日 22:35 猜测这个版面上的常客差不多都不明白这些是啥。

马上有人来证明这话正确

forecasting 写了： 2024年 10月 14日 21:31 有几个定理是关于机器学习的，就是机器能学到什么，什么不可能学到。最初有用形式语言理论表述的，
https://en.wikipedia.org/wiki/E._Mark_Gold
https://en.wikipedia.org/wiki/Language_ ... _the_limit
后来有所谓VC维数， https://en.wikipedia.org/wiki/Vapnik%E2 ... _dimension
​
​机器数学证明是另外一个问题，就是靠人的智能编程实现的机器证明。先说个有关而不不是数学定理机器证明的有Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry%E2% ... espondence
再说数学定理机器证明的几个结果：数理逻辑里的量词消去法和与之相关的Tarski–Seidenberg theorem（https://en.wikipedia.org/wiki/Tarski%E2 ... rg_theorem），还有源自代数几何的希尔伯特零点定理的Buchberger算法（https://en.wikipedia.org/wiki/Buchberger%27s_algorithm）。这些有很多已经超出了机器可学习的上限。但是是机器能证明的。把这些嵌入AI里面，能扩展DNN机器证明的能力，可这些不是机器学到的。嵌入DNN，比如设计接口以解决DNN和形式化的机器证明的交互问题，即自然语言和所嵌入机器正证明所用形式化语言（数理逻辑表达式或程序语言）的互译问题。
​
数学定理的机器证明和机器可学得（learnability）本不是一回事。机器可学得（learnability）的数学定理的证明最好的结果是机器可学得（learnability）的语言的子集（证明等价于语法分析）。所以证明如果超出了机器可学得（learnability），即不可能学得，那么就只能嵌入，即从外界引入，或者搜索匹配。

​与机器证明，直觉逻辑/构造逻辑，Curry-Howard对应有关的或者进一步的发展的一个纲领是univalent foundations https://www.ias.edu/ideas/2014/voevodsky-origins
https://www.ias.edu/math/sp/univalent/goals
https://www.ias.edu/idea-tags/univalent-foundations
Fields奖得主Vladimir Voevodsky 开创或者倡议的。
与univalent fiundation相关的计算项目：https://ncatlab.org/nlab/show/univalent ... athematics

转：将数学建立在计算机可验证的基础上。他提出“同伦类型论”（Homotopy Type Theory），将拓扑学中的同伦概念与类型论结合，并引入“单值公理”（Univalence Axiom）。这一公理允许数学对象在不同“等价”视角下自动统一，从而简化了高阶结构的表达。更重要的是，该理论为计算机辅助证明（如Coq系统）提供了严格的逻辑基础。2012年，他主导编写的《Univalent Foundations Program》一书系统阐述了这一框架，成为形式化数学的里程碑。
.........
在Univalent Foundations的基础上，Voevodsky发起了“UniMath”项目，旨在将经典数学定理编码为计算机可验证的形式。这一愿景正在由新一代数学家与计算机科学家继承，例如Lean定理证明器的开发便深受其启发。

转chatGPT做的摘要：同伦类型论（Homotopy Type Theory, HTT）是数学家Vladimir Voevodsky及其同事提出的一种结合了类型论和拓扑学概念的数学框架。它在传统的类型论基础上，引入了同伦学（Homotopy Theory）中的思想，特别是同伦和同构的概念，并利用类型论的结构来形式化这些数学对象。HTT不仅为数学提供了一种新的描述方式，也为计算机辅助证明（如Coq系统）提供了理论基础。

核心概念：
类型论（Type Theory）：在类型论中，数学对象被视为类型，程序或证明则是这些类型的元素。类型论为形式化数学提供了强有力的工具，尤其在计算机科学中有广泛应用。

同伦学（Homotopy Theory）：同伦学是拓扑学的一个分支，研究空间之间的连续变形。通过同伦，两个拓扑空间可以通过一种连续变形过程被视为相同的（即有同伦关系）。在HTT中，同伦被用来描述类型之间的等价关系。

单值公理（Univalence Axiom）：这是HTT中的一个重要公理，指出如果两个类型是同构的（或同伦的），那么它们可以被认为是相同的。这个公理使得类型之间的等价关系得到了严格的定义，并简化了高阶结构的表达。

HTT的意义：
简化结构：通过同伦的思想，HTT让我们能够在不同的等价视角下统一数学对象，避免了繁琐的等价关系处理。
形式化数学：HTT为计算机辅助证明提供了坚实的理论基础，支持像Coq这样的定理证明工具，使得复杂的数学定理可以被形式化、验证并计算。
拓扑与类型的结合：HTT将拓扑学中的同伦与类型论中的类型系统结合，使得我们能够在类型论的框架下更自然地处理拓扑学问题。
应用：
HTT已经影响了许多数学和计算机科学领域，特别是在形式化数学和定理证明方面。基于HTT的“UniMath”项目致力于将经典数学定理转化为计算机可验证的形式，而Lean定理证明器等工具也受到其启发。

简言之，同伦类型论通过将类型论与拓扑学的同伦思想结合，提供了一种新的数学表达与证明方式，极大地推动了形式化数学和计算机辅助证明的发展。

DeepSeek关于同伦类型论（Homotopy Type Theory, HTT）的介绍

同伦类型论（Homotopy Type Theory, HTT）是21世纪兴起的一种数学理论，融合了类型论（Type Theory）、同伦论（Homotopy Theory）和范畴论（Category Theory）的思想。它由数学家弗拉基米尔·沃沃德斯基（Vladimir Voevodsky）等人推动发展，旨在为数学基础提供一种新的形式化框架，并揭示类型论与拓扑学之间的深刻联系。

核心思想
类型即空间，项即点
HTT将逻辑中的类型（Type）解释为拓扑空间，类型的项（Term）视为空间中的点。例如，类型 AA 可以对应一个拓扑空间，其项 a:Aa:A 对应空间中的某个点。

相等性的拓扑视角
传统的类型论中，两个项的相等性（如 a = ba=b）通常用命题或证明表示。在HTT中，相等性被解释为连接两点的路径，而所有路径构成的集合（路径空间）对应类型的“同伦结构”。例如，两个点之间的不同路径可能对应不同的“证明方式”。

泛等公理（Univalence Axiom）
这是HTT的核心创新，主张等价的两个类型可以视为相等。具体来说，若两个类型 AA 和 BB 之间存在同伦等价（即连续变形可相互转换），则泛等公理允许将这种等价直接视为类型相等（A = BA=B）。这一公理统一了传统数学中的同构、等价和相等性概念。

高阶归纳类型（Higher Inductive Types, HITs）
通过HITs，可以直接在类型中定义拓扑结构的代数对应物。例如，“圆类型” \mathbb{S}^1S
1
可以通过一个基点和一个回路生成，模拟拓扑学中的圆周。

主要特点
将几何直觉引入逻辑：通过同伦论，为类型论赋予几何直观，使得证明和构造过程可通过“空间变形”理解。

泛等基础：提供一种不依赖集合论的新数学基础，避免罗素悖论等经典问题。

计算可解释性：尽管涉及抽象拓扑，HTT仍保持类型论的计算性质，适用于形式化验证（如Coq、Agda等工具）。

应用与意义
数学基础的形式化
HTT为数学对象（如群、流形）提供了更自然的表达形式，尤其适合处理高维范畴和无穷结构。

自动证明验证
结合证明辅助工具（如Coq-HoTT），HTT可用于严格验证复杂数学定理（如费马大定理的形式化）。

理论计算机科学
类型系统与程序语言设计受益于HTT的几何视角，例如依赖类型和程序等价性的研究。

物理与量子计算
某些研究尝试用HTT的拓扑结构描述量子信息中的高维纠缠态。

挑战与争议
复杂性：HTT的抽象性使其学习曲线陡峭，且实际计算实现仍需优化。

与经典数学的兼容性：如何将传统数学（如分析学）完全纳入HTT框架仍在探索中。

总结
同伦类型论通过统一类型论与同伦论，为数学和计算机科学提供了革命性的视角。它不仅是形式化数学的工具，更可能重塑对“数学对象本质”的理解。尽管尚处发展阶段，HTT已在基础数学、逻辑和程序验证领域展现出深远潜力。