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

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