Доказателство от компютър

От Notices, American Mathematical Society [AMS], четвъртък, 6 ноември 2008 г. Вж. http://www.ams.org/ams/press/hales-nots-dec08.html
******************************
American Mathematical Society [AMS] -- Providence, RI:

Използване на компютри за проверка на математически доказателства

Новите компютърни инструменти притежават потенциала за революция в математическата практика, като предлагат много по-надеждни доказателства на математически резултати, отколкото някога са били възможни в историята на човечеството. Тези компютърни инструменти, на базата на понятието „формално доказателство”, през последните години се използват за създаване на почти безпогрешни доказателства на много важни резултати в математиката. Една революционна серия от четири статии от водещи специалисти, публикувана днес в Notices на American Mathematical Society (http://www.ams.org/notices), изследва новите развития в използването на формалното доказателство в математиката.

Когато математиците доказват теореми по традиционния начин, представят своите аргументи в разказвателен вид. Те представят предишни резултати, нахвърлят детайли, които смятат, че другите специалисти ще разберат, съкращават изложението си, за да го направят по-малко скучно, разчитат на интуицията и т.н. Правилността на аргументите се определя от критичното разглеждане от други математици, в неофициални обсъждания, лекции или списания. Отрезвяващо е да се осъзнае, че начинът, по който се проверяват математическите резултати, е по същество социален процес и поради това е податлив на грешки. Когато става въпрос за важни, добре известни резултати, доказателствата се проверяват много добре и грешките в крайна сметка се откриват. Въпреки това историята на математиката познава много случаи на грешни резултати, които са останали неразкрити дълго време. Освен това, в някои случаи напоследък важни теореми са изисквали толкова дълги и сложни доказателства, че много малко хора разполагат с времето, енергията и необходимия опит, за да ги проверяват внимателно. А някои доказателства съдържат обширен компютърен код, например за проверка на много случаи, които иначе не биха могли да се проверят ръчно. Как математиците могат да бъдат сигурни, че тези доказателства са надеждни?

За да заобиколят тези проблеми, компютърните специалисти и математиците започнаха да разработват съвместно областта на формалното доказателство. При формалното доказателство всяко логическо заключение се проверява назад до основните аксиоми на математиката. Математиците обикновено не пишат формални доказателство, защото те са толкова дълги и тежки, че е невъзможно да бъдат проверени от хора математици. Но сега вече разполагаме с „асистенти за компютърно доказателство”, които извършват проверката. През последните години асистентите за компютърно доказателство станаха достатъчно мощни, за да се справят с най-различни доказателства.

Само в някои прости случаи на асистента за компютърно доказателство може да се подаде дадено твърдение и да се очаква, че той ще предложи доказателство. По-скоро математикът трябва да знае как да докаже твърдението, а след това доказателството се доразвива в голяма степен чрез специалния синтаксис на формалното доказателство, в което се изписва всяка стъпка, и точно това формално доказателство се проверява от компютъра. Възможно е също така да се даде на компютрите свобода да изследват математиката самостоятелно и в някои случаи те са давали интересни предположения, останали незабелязани от математиците. Възможно е да сме близо до момента, в който по-скоро компютрите, а не математиците, ще правят математика.

Четирите статии в Notices разглеждате сегашното състояние на формалното доказателство и дават практически съвети за използването на асистенти за компютърно доказателство. Ако използването на тези асистенти се разпространи, те биха могли да променят дълбоко математиката в настоящия й вид. Една дългосрочна мечта е да получим формални доказателства на всички важни теореми в математиката. Томас Хейлс – един от авторите, пишещи за Notices – казва, че една такава сбирка от доказателства ще представлява сама по себе си „определяне на математическия геном”.

Четирите статии са:

Formal Proof, by Thomas Hales, University of Pittsburgh

Formal Proof---Theory and Practice, by John Harrison, Intel Corporation

Formal proof---The Four Colour Theorem, by Georges Gonthier, Microsoft Research, Cambridge, England

Formal Proof---Getting Started, by Freek Wiedijk, Radboud University, Nijmegen, Netherlands

Статиите излизат днес в декемврийския брой за 2008 г. на Notices и са свободно достъпни без абонамент. За допълнителна информация:

Professor Thomas Hales
Department of Mathematics
University of Pittsburgh
Email: hales@pitt.edu

American Mathematical Society
Public Awareness Office
201 Charles St.
Providence, RI 02904
Email: paoffice at ams dot org
Phone: 401-455-4000
Fax: 401-331-3842
 

Виртуален
училищен
кабинет по
математика

Квалификационни
курсове за
учители