Мнение 37: Познай какво? Програмирането е дори по-забавно от доказването и, по-важното, дава също толкова, ако не и повече, разбиране и прозрения

От Дорон Зайлбергер
Написано: 15 април 1999 г.

След позорното отхвърляне на моето провокативно, но непреднамерено такова, Мнение 36 от редакторите на Notices of the AMS, си позволих да го разпространя по имейл и се съгласих с брилянтната идея на моя студент Арън Робъртсън да го публикува на sci.math и sci.math.research.

Реакциите бяха интересни, някои от които публикувах в секцията за обратна връзка. Благодаря особено на Андрей Бауер и Рон Брук за силните им аргументи.

Тук бих искал да уточня предишното си "силно" мнение и да реагирам на реакциите, като цяло.

Моето ИСТИНСКО мнение е, че човешкото доказване и програмирането на компютри за доказване са еднакво важни и заслужаващи. Съгласен съм с Хаминг, че ролята на изчисленията е в прозренията, а не в числата или символите. НО, тъй като 99 процента от работещите математици не знаят как да програмират, направих го драматично, за да ви накарам да действате...

... Но понякога прекалената настойчивост води до обратен ефект, предполагам.

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

И сега, чуйте, вие всички самоправедни защитници на прозренията и разбирането. Едно добро доказателство може да създаде впечатление за разбиране, но ЗА ДА РАЗБЕРЕТЕ НЕЩО НАИСТИНА ДЪЛБОКО, ТРЯБВА ДА ГО ПРОГРАМИРАТЕ.

Когато искам да науча нов предмет, обявявам курс за магистри и докторанти по него, защото най-добрият начин да научиш нещо е като го преподаваш. Но дори по-добро от преподаването на хора е преподаването на компютри, т.е. програмиране! Защото компютрите няма да ви позволят да импровизирате.

Може би наистина е вярно, че цялата математика един ден ще бъде напълно автоматизирана, но тази част от моята прогноза беше само за драматичен ефект. Нямам мнение по въпроса за силния или слабия ИИ и не обичам да говоря за политика или религия. Говорех главно за краткосрочната перспектива — за това как трябва да правим изследвания сега. А текущите работни навици на повечето математици са много неефективни и неадекватни, тъй като все още имат мислене от епохата преди компютърната алгебра.

... За краткосрочната цел да постигнем възможно най-много математическо ПРОЗРЕНИЕ и РАЗБИРАНЕ през нашия живот, трябва да научите как да програмирате в Maple, Mathematica и други подобни. Зная, че е много болезнено да учиш нещо ново, но веднъж щом преминете през това, ще ми благодарите! Ще осъзнаете, че НАИСТИНА разбирате нещо САМО след като го ПРОГРАМИРАТЕ САМИ.

Друга човешка слабост е микромениджмънтът на детайлите на доказателствата. Жалко за онзи, който мисли, че доказателствата на Апел-Хакен или Хейлс[1] не дават никакви прозрения. Разбира се, самите детайли не го правят, но кого го интересува? Важен е общият подход, въплътен в КОМПЮТЪРНАТА ПРОГРАМА, която е изпълнена с прозрения. Единственият ми проблем с доказателствата за 4CT (теоремата за четирите цвята) е, че включват твърде много човешка проверка. Най-доброто доказателство трябва да е напълно автоматизирано, а човекът просто да се наслаждава на програмата.

Друга погрешна представа е, че сорс-кодът е по-труден за четене от човешкото доказателство. Нелепо. Добре написана, модулна и добре документирана компютърна програма е много по-лесна и по-забавна за четене, отколкото дълго човешко доказателство.

Каква беше главната причина, че аз се мъчих да напиша RENE? Да науча геометрия! Сега съм цар на равнинната геометрия. И сега имам конкретното и дълбоко чувство, че всичко това е рутинно.  Въпреки, че геометрията, базирана на триъгълници не е на мода в днешно време, тя беше много уважавана допреди осемдесет години и ми дава такъв кеф, че писането на команда Morley() доказва теоремата на Морли само за няколко секунди. Забавното е, че Ален Кон наскоро създаде наистина красиво доказателство от три страници. Но това, което Рене Декарт вече е знаел и бе направено явно с моя пакет в Maple RENE е, че всичко това е рутинно.  Можете ли да си представите Ален Кон да напише статия озаглавена „Ново доказателство на 21x31=651”?

Така, че RENE е просто метафора на нарастващата рутинизация на математиката.

По-нов пример е така наречената WZ теория. Само преди десет години двама водещи комбинаторици, Ира Гесел и Денис Стантън, публикуваха статия (в JCT(A)): „Кратки нови доказателства на равенствата на Диксън и Заалшутц“. Сега, благодарение на WZ, те имат същия епистемологичен статус като 1+1=2. Друг пример е алгоритмичната теория на решетката на Марк Хайман.

Изключително малко вероятно е тези да са единствените примери. Така че една много ИНТЕРЕСНА и ЗАБАВНА дейност би била да се опитаме да тривиализираме и рутинизираме (или по-деликатно казано, алгоритмизираме) колкото се може повече от познатата математика. Когато го направите, става безсмислено да се разбира например идентичността на Диксън. Тя е истинна просто ЗАЩОТО е такава. Но ГЛОБАЛНОТО разбиране, че изразът на Диксън, подобно на стотици други, е вграден в алгоритмична рамка, е наистина интересното нещо.

 

Всъщност, изразът на Диксън беше лош пример. Доминик ФОАТА даде великолепно комбинаторно доказателство, което промени живота ми и доведе, заедно с еднакво елегантното доказателство на Айра Гесел за оценката на детерминантата на Вандермонд, до моето основополагащо доказателство, с Дейв Бресу, на все още нерутинната q-хипотеза на Дайсън.

Така че, наистина, ЧОВЕШКИТЕ доказателства все още са добре дошли. Но трябва да повишим стандартите. Красивото доказателство на Фоата е бижу, но 99.9 процента от другите доказателства са по-лоши от доказателствата на Шалош Б. Екад (псевдоним за неговия компютър – бел.прев).

Също така доказателството на Кон за теоремата на Морли е такава красота, че си струва да се прочете, въпреки че теоремата може да се провери с Maple за 3 секунди. НО всички онези многословни решения на задачи от Monthly не са!

Друго предимство за хуманитаристите сред нас е следното. Когато част от математиката стане рутинна, трябва да потърсим замяна. Така че една добра изследователска програма е следната циклична конструкция:

Do

{

тривиализираме и рутинизираме цялата позната математика;

откриваме нови нетривиални части от математиката;

}

while(докато сме живи)

И така, поуката е да прекратим тази глупава борба, да се помирим и да работим заедно! Фоата и Кон наистина трябва да продължат да измислят красиви и проницателни човешки доказателства, които дори когато доказват рутинни факти, биха могли много добре да се обобщят до доказателства на нетривиални факти. НО, с ЕДНАКВО ВРЕМЕ и УСИЛИЯ, нека играем ИГРАТА НА ТРИВИАЛИЗИРАНЕ. А за това е по-добре да се научите да ПРОГРАМИРАТЕ в Maple.

 

Да завърша с цитат от Борвейн, Борвейн, Гиргензон и Парнес (Math Intell. Есен 1996, стр. 15): "Защо Зайлбергер е толкова склонен да се откаже от абсолютните истини? Най-разумният отговор е, че той преследва по-дълбоки истини".

По аналогия, трябва да се откажем от локалното микроуправление на "разбиране" на отделните факти, в полза на ГЛОБАЛНО инфраструктурно разбиране. И за това ТРЯБВА да научим как да ПРОГРАМИРАМЕ!

 

 

 

 

 

 

 

 

 

 

 

[1] Доказателства, извършени с помощта на компютър. Апел и Хакен доказват теоремата за четирите цвята с помощта на пълно изброяване на случаите с компютър, резултатът е нечетим за човека. Хейлс използва сходен подход за доказателство в областта на комбинаториката.

ne e lo6a ideia tova s programiraneto