科研之友
微信
新浪微博
Facebook
分享链接
摘要
RECENT PROGRESS IN automated reasoning and super-computing gives rise to a new era of brute force. The game changer is "SAT," a disruptive, brute-reasoning technology in industry and science. We illustrate its strength and potential via the proof of the Boolean Pythagorean Triples Problem, a long-standing open problem in Ramsey Theory. This 200TB proof has been constructed completely automatically-paradoxically, in an ingenious way. We welcome these bold new proofs emerging on the horizon, beyond human understanding-both mathematics and industry need them.
- 出版日期2017-8
