(no subject)

[singalen]

Надеюсь, Вова не против, что я про это напишу.

muwlgr:
    

Компьютер наконец-то начал приносить пользу математикам

    В смысле, некую нетривиальную пользу именно за счёт способности
    перелопачивать большие объёмы информации в процессе
    автоматической верификации доказательств.
    Т.е. сделан ещё один маленький шажок поближе к Сингулярности :>

Действительно выдающийся результат.

Интересно, что Flyspeck - опенсорсный софт, а в академической среде опенсорс распространяется на ура.
И если толпа обезьян студентов навалится печатать в него или в HOL Light условия всяких теорем, то есть шанс, что какая-то часть расколотых машинным способом теорем будет ещё не доказана людьми.

Вот вам и иллюстрация, пожалуйста: http://code.google.com/p/flyspeck/wiki/HolLightDemo1

В статье поминают, что сейчас большая проблема - инженерия знаний: мы пользуемся при рассуждении уймой приёмчиков, которые никто никогда не формализовал.

// HOL Light написан на OCaml, Flyspeck - на Java.
// // Встречалась мне когда-то веб-страничка размером в парсек - там был явно прописан размер. Как ни гуглю, не могу найти. Кто может? :)

Comments

[muwlgr.livejournal.com]

Я обычно "за". Даже стишок на своём ЖЖ-заголовке недавно поменял - http://muwlgr.livejournal.com/436.html :>

[deni-ok.livejournal.com]

В декабре был целый выпуск Notices of the American Mathematical Society A Special Issue on Formal Proof (http://www.ams.org/notices/200811/)