Computer Proofs [Romanian]

Original in English by Sara Billey

Dovezile calculatorului

Care este valoarea dovezilor asistate de calculator?

Evident, valoarea unei dovezi asistate de calculator constă în aceea că ştim cu exacitate că rezultatul este adevărat! Nu putem construi o teoremă până când nu vom şti că ea fost verificată. În scopul dezvoltării matematicii, avem nevoie sa folosim toate instrumentele pe care le avem, uneori înseamnă că avem nevoie să ne bazăm pe dovezile asistate de calculator. Deci, aşa să fie.

Unii matematicieni au încercat să protejeze ego-urile lor, spunînd că dovezile umane sunt mai superioare decît dovezile asistate de calculator. Ei spun că noi nu învăţăm mai mult din dovezi asistate de calculator aşa cum asta poate face un om.  Opinia lor – dovezile calculatorului va fi dificil de verificat. Pentru ei, dovezile computerului sunt mai puţin elegante. Eu am găsit aceste plângeri naive.

În opinia mea, dovezi asistate de calculator sunt revoluţionare. Fiecare probă de calculator nouă este un exemplu din care putem învăţa ceva nou. Aceasta este o tehnică nouă în istoria matematicii. Noi nu ne-am născut ştiind cum să aplicăm inducţia şi fără de a ști cum să creăm o probă de calculator asistată corespunzătoare. Avem nevoie să vedem o mare varietate de exemple înainte să folosim confortabil această tehnică. Avem nevoie să cunoaștem domeniul de aplicare ale problemelor care pot fi supuse la asistenţa calculatorului. În scopul de a aprecia eleganţa acestor dovezi și probe şi a stabili standarde pentru publicare avem nevoie de argumente pentru a citi în mod clar rezultate şi algoritmi care dovedesc teoreme prin intermediul acestei noi metode.

Toate dovezile asistate de calculator trebuie să fie scrise în mod corespunzător, în scopul de a câştiga mai multă acceptare. Porţiunea calculatorului în probei ar trebui să includă un algoritm bine documentat, care poate fi pus în aplicare în orice limbă de calculator şi, în orice sistem de operare. Împlementînd mai multe persoane diferite putem mări încrederea cititorului, la fel ca avînd mai mulți arbitrii. Jurnale și reviste nu pot publica milt cod de computer, dar este uşor de a face cod disponibil pe un site web.Codul pentru o dovadă asistată de calculator trebuie să fie bine documentată şi ATENT TESTATĂ. Standarde ridicate pentru testarea codului în dovezile asistate de computer nu pot fi subestimată.

Ce tipuri de teoreme pot fi supuse la probe asistate de calculator? Acest lucru este greu de spus în acest moment. Sunt uimit de matrice a rezultatelor care au fost deja date de calculator. De exemplu, dovada lui Hales a conjecturii lui Kepler (Hales proof of the Kepler conjecture) este o victorie reală, deoarece este foarte dificil să determinăm un număr transcendental cu calculatorul în cazul în care întotdeauna există o problemă cu eroare rotunjită. WZ-metoda de a dovedi identitatea pe serii hipergeometrică este frumos descrisă în cartea A=B de Petkovsek, Wilf şi Zeilberger. Cea mai recentă dovadă a Teoremei 4 culori (4 Color Theorem) de Robertson, Sanders, Seymour şi Thomas este un exemplu perfect a unei dovezi bine scrise şi asistate de calculator; partea scrisă a probei este de aproximativ de 18 pagini, codul computerului generează întregul set reductibil/inevitabil însuși astfel încât nu sunt necesare intrările omului grafice. Codul a fost implementat de către mai multe persoane în mai multe limbi. Ca un ultim exemplu de dovezi asistată de calculator, putem numi pe cele lui Postnikov şi eu am arătat că varietațile lui Schubert pentru toate semnale multiple G/B, cu G, fiind un grup simplu lui Lie complex care poate fi caracterizat folosind eficient model de evitare generalizat (generalized pattern avoidance).

Ce încă putem învăța de la o probă de calculator? Ei bine, fiecare astfel de probă sau dovadă conţine un fel de miracol care face posibil de a verifica prin calculator. De exemplu, este absolut un miracol că teorema a 4 culori poate fi dovedită prin calculator, deoarece ar fi putut fi cazul, cînd orice mulţime reductibilă/inevitabilă are dimensiunea de cel puţin 10 ^ 50. Dar nu, într-un fel algoritmul lui Seymour, Robertson, Sanders și  Thomas a găsit un set reductibil/inevitabil cu numai 631 elemente. Asta nu e nimic pentru un calculator! Aceste minuni nu sunt teoreme de sine stătătoare, dar ele sunt leme în ierarhia noastră obişnuită a lemelelor, propunerilor şi teoremelor. Ei ne spun ceva despre complexitatea obiectelor cu care lucrăm. Ei adauga ceva la intuiţia noastră şi în perspectivă matematică.

La multe conferinţe şi seminare, am auzit cu toţii cum cineva anunță prima dovada “ geometrică de o teoremă din cauza aşa-şi-aşa'', sau “prima dovadă pur combinatorică''sau prima dovada “algebrică'', etc. De a dovedi teoreme folosind diferite instrumente este foarte util pentru că ajută la conectarea lucrurlui în alte domenii ale matematicii. Aceasta poate face astfel de probe accesibile pentru un public mai larg, şi să încurajeze descoperirea noilor instrumente. Cu toate acestea, noi nu auzim de multe ori oamenii vorbind despre prima dovadă “de asistată calculator'' în orice rezultat cunoscut.Dovezi de calculator sunt dispreţuite de mulți matematicieni, și ei acordă numai cele dovezi atunci când este cunoscut că e o dovadă a “omului''. Este o greşeală să dispreţuim cea mai utilă invenţie matematică văzută de la inventarea creionului.

Vreau să vă provoc să luați în considerare încercarea de a dovedi unele rezultate de calculator cât curând e posibil, în scopul de a practica tehnica. Tehnici de dovadă a calculatorului sunt în faza de început în ziua de azi. Ele nu sunt predate în acelaşi mod în care noi invățăm alte metode de probă, cum ar fi inducţia, dovada de contradicţie, sau dovezi contrapositive. Dispunem doar de metode euristice, chiar şi pentru recunoaştere atunci când o teoremă este cedată la calculator ca o dovadă în majoritatea domeniilor. Trebuie să dezvoltăm abilităţile noastră învățînd de la calculator, astfel dovedind încât putem profita de această invenţie uimitoare atunci când ne este necesar. Noi trebuie să explorăm drumul spre o dovadă a calculatorului bună, deoarece aceasta va duce spre o matematică bună. Noi trebuie să stabilim standarde pentru publicarea dovezilor asistata de calculator atunci când revista nu poate include tot conținutul codului. Trebuie să încurajăm matematicienii a cărora cercetarea de pionierat îmbrăţişează această abordare nouă şi ne oferă mai multe exemple pentru a învăţa de la ea. Pentru a încuraja explorarea în domeniul de probă asistată de calculator, noi ne întrebăm: "Există oare o dovadă de calculator şmecher asistată a teoremei lui Fermat?"

Premiu de 500 dolari

Un premiu cash de $ 500 este oferită pentru o dovadă asistată de calculator a teoremei lui Fermat, care poate fi descrisă într-un articol de 20 pagini sau mai puţin, iar articolul este acceptat în orice revistă de specialitate matematică subscrisă de la Universitatea din Washington. Acest articol trebuie să fie scris în limba engleză pentru a revendica premiul.

Dacă alţii ar dori să contribuie la premiul, voi începe să strîng o colecţie.

ok ok