我最近也在看这个,工业界的应用主要是写出可信的无bug的程序,数学家的话用来确保一些很复杂的证明是可信的没有gap,现有比较有名的例子是四色定理和奇阶定理(odd order theorem)

【 在 Sunyata (水木诗妖龙静颜) 的大作中提到: 】
: 是法国人发明的，coq就是法语公鸡，高卢公鸡。
: 我看到科普，说这玩意是人工智能可以搞机器证明。
: 后来看了本教程，看来看去看不懂（＃－.－）
: ...................
--
修改:annals FROM 123.118.114.244
FROM 123.118.114.244

工业界可信的都不是编译型的，都是解释型的，例如波音和空客航空器使用软件系统。




【 在 annals 的大作中提到: 】
: 我最近也在看这个,工业界的应用主要是写出可信的无bug的程序,数学家的话用来确保一些很复杂的证明是可信的没有gap,现有比较有名的例子是四色定理和奇阶定理(odd order theorem)
:
--
FROM 111.18.168.*

coq不是搞自动证明,而是辅助证明,目标不一样

以及现在有可信的c编译器

【 在 SmartIC (SmartIC) 的大作中提到: 】
: 基于AI的机器证明，已经搞到头了，至少该挖的金矿都挖了。
--
FROM 123.118.113.99