类型论与形式证明

Hacker News 上怎么说

• codeismath · 2021 年

  我发现《Type Theory and Formal Proof》的前6章在讲类型论背后的基础数学方面简直太棒了。作者（Nederpelt 和 Geuvers）没有掩盖任何假设，而是一步一步抽丝剥茧。我大学里没学过这些……

  I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university…

• nicklaf · 2021 年

  ……（来自逻辑学家的）其实相当直白，论文在概念上也不见得有多难，主要是抽象层次层层叠叠。顺便提一句，关于这个话题有人向我推荐了 Nederpelt 和 Geuvers 写的《Type Theory and Formal Proof: An Introduction》。我还没机会深入学，但我觉得值得一看。

  …from logicians) are actually quite straightforward, and the papers are not necessarily conceptually difficult so much as layered in their use of abstraction. I'll mention that Nederpelt and Geuvers' Type Theory and Formal Proof: An Introduction was recommended to me for this topic. I haven't had a chance to study it yet, but I'd say it's worth checking out.

• codeismath · 2025 年

  书单。我书架上涵盖这些主题的一些书：Simon Thompson 写的《Type Theory and Functional Programming》（搜一下就能找到 PDF）；Rob Nederpelt / Herman Geuvers 写的《Type Theory and Formal Proof》前120页；想看依赖类型（dependent types）早期资料的话（上面那本也有涉及），可以看看 Per Martin-Lof 的《Intuitionistic Type Theory》；还有《Computation and Reasoning: A Type Theory……

  Books. Some books on my shelf covering these topics: "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search) First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof "Computation and Reasoning: A Type Theory…

• griffzhowl · 2025 年

  我最近对数学形式化产生了兴趣，发现 Nederpelt 和 Geuvers 写的《Type Theory and Formal Proof》真是一本好书，它带你从无类型 lambda 演算出发，逐步扩展类型系统，直到构建出完整的依赖类型论（dependent type theory）和构造演算（Calculus of Constructions）……

  I've got interested in formalization of mathematics recently and found the book Type Theory and Formal Proof by Nederpelt and Geuvers is a really nice one, taking you from the untyped lambda calculus and gradually extending the type system until you get the full dependent type theory and the Calculus of Constructions…

• LightMachine · 2026 年

  ……它……Bend 的理论涉及多个领域（依赖类型、次结构类型、停机性）。然后还有运行时、编译器、GPU kernels……如果你专门指类型论的话，Nederpelt 和 Geuvers 写的《Type Theory and Formal Proof》是一本很好的入门书。线性类型方面我不确定推荐什么好，据我所知没什么书是非常基础入门的？也许《Idris 2: Quantitative Type Theory in Practice》算，那本是……

  …it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels... If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is…

• roadside_picnic · 2026 年

  ……把两个不同领域（LLM 和定理证明）的前沿成果结合起来的模式，绝对有潜力从根本上改变数学研究的方式。《Type Theory and Formal Proof》第381页有一张很棒的图，你能很清楚地看到 LLM 可以被放在那张图里最棘手的两个环节来解决问题。因为工作是经过形式化验证的，我们可以直接甩掉整整几大类 LLM 带来的问题（比如幻觉）。……

  …pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve. Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations).…

正在加载完整评论……