Сметачки потпомогнат доказ

Сметачки потпомогнат доказ — математички доказ кој е делумно создаден од сметачот.

Повеќето сметачки потпомогнати докази за датумот се имплементации на големи докази по исцрпување на математичка теорема. Идејата е за да се користи сметачка програма која што ќе ги врши долгите пресметки, и со тоа обезбедува доказ дека резултатот од овие пресметки ја имплицира дадената теорема. Во 1976 година, четирибојната теорема беше првата голема теорема која беше потврдена со помош на сметачка програма.

Направени се обиди во областа на вештачката интелегенција за да се создадат, нови, експлицитни и помали докази на математичките теореми. Како и автоматските докажувачи на теореми докажале поголем број на нови резултати и пронашле нови докази за познати теореми. Покрај тоа интерактивните докажувачки асистенти им овозможиле на математичарите да развијаат читливи докази кои се официјално потврдени за коректност. Иако овие докази може да се проверат од човек, тие не ги делат коннтраверзните импликации на сметачки потпомогнатите докази.

Методи

Еден метод се користи во докази поврзани со бројчени пресметки. Притоа се контролира грешката на заокружување и натрупувањето на грешките во интервалот на аритметичката техника. Поточно едно намалување на пресметките на секвенцата на основните оерации(+,-,*,/) резултира на елементарните операции кои се заокружени со сметачка прецизност. Сепак, може да се конструираат интервали обезбедени од горните и долните граници на резултатите на елементарната операција. Потоа една придонесува со заменувањето на броевите со интервали и вршење на основните операции помеѓу истите.

Филозофски забелешки и приговори

Сметачки потпомогнатите докази се предмет на многу контроверзи на математичкиот свет. Некои математичари сметаат дека долгите сметачки потпомогнати докази не се, во извесна смисла, 'вистински' математички докази, бидејќи тие подразбираат многу логични чекори кои не се практични да се верификуваат од човечките битија и математичарите ефикасно се трудат да го заменат логичкото одбивање од претпоставената аксиома со доверба во емпириски пресметковен процес, кој е потенцијално погоден од грешките во сметачката програма, како и дефекти во траењето во животната средина и хардверот. Другите математичари сметаат дека сметачките потпомогнати докази треба да се сметаат како пресметки, наместо докази: алгоритамскиот доказ сам треба да се докаже валиден така што неговата употреба тогаш може да се смета како проверка. Ова е познато како 'принципот Поенкаре' во математичката заедница по изјавата на Анри Поанкаре. Аргументите за сметачките потпомогнати докази се предмет на грешки во нивниот извор на програми, компајлери и хардвери. Друг можен начин на верификување на сметачките асиститирани докази е да се гарантираат нивните расудувани чекори во машински читлива форма, а потоа се употребува автоматски услужник за теореми за да ја покажат својата коректност. Овој пристап на користење на сметачка програма за да се докаже друга програма, не е за да се задоволат скептиците на сметачките докази кои тоа го гледаат како додавање на уште еден слој на сложеност без да се согледа потребата за човековите сфаќања. Друг аргумент против сметачките потпомогнати докази е дека тие немаат математичка елеганција-кои ги обезбедуваат, немаат увид за нови корисни концепти. Дополнителни филозофски прашања од страна на сметачките докази е дали тие се направи во математичка квазиемпириска наука, каде што на научниот метод станува поважен од примена на чист разум во областа на апстрактните математички концепти. Ова се однесува директно на аргументот во рамките на математиката за тоа дали математиката е врз основа на идеи, или "само" на една вежба во официјалниот симбол на манипулацијата. Таа исто така го покренува прашањето ако се насочите според гледањето на Платонистите, сите можни математички предмети во извесна смисла "веќе постојат", дали сметачки-потпомогнатата математика е наука заснована на набљудување како астрономијата, повеќе отколку експериментална како физика или хемија. Интересно, во рамките на физичката заедница истовремено се поставува прашањето дали дваесет и првиот век теоретската физика треба да стане премногу математичка, и оставајќи ги зад себе своите експериментални корени.

Список на теореми докажани со помош на сметачки програми

Вклучувањето во овој список не повлекува дека постои формален доказ проверен со сметач, туку повеќе дека сметачка програма е употребена на некој начин. Видете ги главните статии за повеќе детали.

Теорема на четори бои, 1976
Connect Four, 1988 – игра
Непостоење на конечна проективна рамнина од ред 10, 1989
Robbins conjecture, 1996
Kepler conjecture, 1998 – проблемот на оптимална сфера спакувана во кутија. Сè уште не е комплетно докажана.

Додатна литература

Lenat, D.B., (1976), AM: An artificial intelligence approach to discovery in mathematics as heuristic search, Ph.D. Thesis, STAN-CS-76-570, and Heuristic Programming Project Report HPP-76-8, Stanford University, AI Lab., Stanford, CA.

Надворешни врски

Edmund Furse; Why did AM run out of steam? Архивирано на 28 мај 2006 г.
Keith Devlin; Last doubts removed about the proof of the Four Color Theorem, MAA Online, January 2005
Number proofs done by computer might err Архивирано на 29 јуни 2011 г.
„A Special Issue on Formal Proof“. Notices of the American Mathematical Society. December 2008.