Matematika pruvo

Ĉi tiu artikolo estis Artikolo de la semajno! — Aliaj Artikoloj de la semajno

---

Pruvo de aserto, ke ĉiu segmento estas flanko de iu egallatera triangulo , devenanta el bazoj de Eŭklido. Unu el la plej malnovaj konservitaj matematikaj pruvoj.

En matematiko pruvo estas demonstro de senduba valideco de iu aserto surbaze de certaj supozoj (aksiomoj).

La matematika pruvo devas esti eksplicite bazita sur nedubeblaj reguloj de prudenta rezonado (tiaj reguloj estas esprimataj en matematika logiko en formo de aksiomoj de logiko), kiu allasas nenian procedon bazitan sur opinio, eksperimento, intuicio aŭ sperto.

Tiuj ĉi ecoj igas matematikan pruvon la plej rigora el la konataj manieroj kontroli validecon de iu ekzakte formulita aserto. Tamen la samaj ecoj faras la matematikan pruvon tute ne eluzebla en aliaj terenoj, ol en matematiko mem.

La aserto, por kiu estas konata matematika pruvo, nomiĝas teoremo.

Principo de matematika pruvo

Eblas aserti, ke la nocio de rigora matematika pruvo estas tio, per kio la matematiko karakterize dividiĝas el la spektro de ceteraj sciencaj disciplinoj.. La matematika pruvo estas nome diference de pruvoj en aliaj terenoj de homa farado (ekz. en juro, naturscienco ktp.) almenaŭ principe nedubebla . Ne estas eliminite, ke oni sukcesos matematike pruvi teoremon, kiu fakte ne validas. Sed poste la pruvo de tiu ĉi teoremo devas esti devige erara kaj tiu ĉi eraro devas esti (post sufiĉe longa esplorado) trovebla. La fonto de eraroj dum la matematika pruvado do ne estas la nocio de pruvo mem, sed ĉiam kaj sole erarantaj homoj.

Indukta kontraŭ dedukta pruvado

Pli detalaj informoj troveblas en artikoloj Indukta logiko kaj Dedukta logiko.

Indukta pruvado

En ĉiuj sciencaj disciplinoj escepte de la matematiko la teorioj estas prijuĝataj laŭ mezuro de harmonio kun la reala mondo kaj laŭ tio, kiom ili kapablas klarigi kaj antaŭvidi realajn aperaĵojn. Novaj teorioj estas konstruataj tiel, ke ili respondu al eksperimente certigitaj datumoj. Se ili harmonias kun tiuj ĉi datumoj, ili estas proklamitaj kiel ĝustaj. Se estas post ia tempo elparolita hipotezo, pri kies valideco la nuntempa teorio ne kapablas decidi, estos farita eksperimento, laŭ kies rezulto tiu ĉi hipotezo estos aŭ rifuzita aŭ ĝi estos enkonstruita en la agnoskatan teorion. Se pli poste aperos eksperimentaj datumoj, kiuj estas en disputo kun la ekzistanta, tiu ĉi teorio estas repuŝita kaj anstataŭita per la nova teorio. Tiu ĉi maniero de la verkontrolado de la hipotezoj kaj la konstruado de teorioj nomiĝas la indukta.

Ekzemplo de indukta pruvo povas esti maniero de kaŭzigo de aserto "Morgaŭ matene leviĝos la suno." El niaj spertoj kaj el spertoj de niaj antaŭuloj ni scias, ke la suno jam multmilfoje leviĝis. Kontraŭ tio ni havas neniajn informojn pri tio, ke la suno iumatene ne leviĝus. Plie la suno lastatempe montras nenian nekutiman konduton, kiu respondus al tio, ke io estas kun ĝi alie, ol kiam ajn en la registrita historio. Surbaze de tiuj ĉi faktoj ni do venos al konkludo, ke kun tute neglektebla ebleco de eraro la suno morgaŭ matene denove leviĝos.

Sed la indukta pruvado povas esti tre perfidema. Ekzemple en klasika mekaniko ĝi estas akceptata kiel vera aserto konata kiel la dua leĝo de Newton pri movado, kiu asertas: "Se al korpo efikas forto, tiam la korpo moviĝas per akcelo, kiu estas proporcia al la efikanta forto kaj inverse proporcia al la maso de la korpo." Tiu ĉi aserto respondis ĝis la dua duono de la 19-a jarcento al ĉiuj farataj eksperimentoj kaj ĝi estis do konsiderata kiel vera - indukte pruvita. Post tio, kiam je interŝanĝo de la 19-a kaj la 20-a jarcentoj kelkaj eksperimentoj pruvis, ke la movo de lumo ne direktas sin per la leĝoj de Newton, tiu ĉi aserto estis komune kun la tuta klasika mekaniko rifuzita kaj anstataŭita per teorio de relativeco. Laŭ tiu ĉi teorio la forto efikanta al la korpo moviĝanta per rapideco proksima al rapideco de lumo kaŭzas nur minimuman akcelon kaj la reston de la enmetita energio kaŭzas pligrandigon de la maso de korpo.

El la lasta ekzemplo evidentas, ke indukte pruvita aserto povas esti neniam konsiderata kiel tute nedubebla. Neniu, eĉ maksimuma kvanto da eksperimentaj datumoj konfirmantaj tiun ĉi aserton nome povas certigi, ke ia en estonteco farita eksperimento ne estos kontraŭ ĝi en disputo.

Dedukta pruvado

Kontraŭe al tio la dedukta pruvo estas tia, en kiu la donita aserto estas pruvita laŭ difinitaj supozoj sole surbaze de de logikaj konsideroj. Plie tiuj ĉi logikaj konsideroj estas dividitaj en fine multaj paŝoj, el kiuj en ĉiu estas derivita sole unusola aserto senpere rezultanta el la antaŭe derivitaj. El tiuj ĉi motivoj estas la dedukte pruvita aserto vera, se estas veraj supozoj, el kiuj ĝi estis derivita. Tiu ĉi vereco estas plie tute nedubebla, ĉar la pruvo eblas dividebla en fine multajn paŝojn, el kiuj ĉiu estas senpera logika sekvo de la antaŭe pruvitaj asertoj kaj kiel tia do nedubebla.

Ĉiuj specoj de la matematikaj pruvoj ekde la historiaj komencoj de tiu ĉi nocio mem en antikva Grekio ĝis la nuntempo, tra la tuta vasteco de la plej diversaj pruvmetodoj, estas deduktaj pruvoj.

Ekzemploj de induktaj kaj deduktaj pruvoj de matematikaj asertoj

Produto de du neparaj nombroj estas nepara

Ni konsideru aserton: "Produto de ĉiuj du neparaj naturaj nombroj estas nepara natura nombro."

Se ni provos kelkajn malaltajn naturajn nombrojn, ni konstatos, ke la aserto validas por ili: 1 · 1 = 1; 1 · 3 = 3; 3 · 1 = 3; 3 · 3 = 9; 3 · 5 = 15; ... Simile ni ekzemple helpe de uzo de komputilo povus verkontroli, ke la aserto validas por ĉiuj nombroj malpli grandaj ol 1 000 000, se tio ne sufiĉus al ni, ni povus plialtigi tiun ĉi limon libervole alten, ekzemple al 10^{1 000 000} (nombro komencanta per unuo, malantaŭ kiu sekvas 1 000 000 nulojn), kaj ĉiam ni konstatus, ke la aserto validas. Post certa tempo de tiaj ĉi plialtigoj de la limo ni jam povus agnoski, ke ni estas provintaj sufiĉe da ekzemploj por tio, por ke ni estu preskaŭ centprocente certaj pro la ĝusteco de nia aserto. Ni pruvis tiun ĉi aserton indukte. Sed ni neniam povas esti tute certaj, ke ia kontraŭekzemplo ne situas senpere post la nombro, kun kiu ni finis la testadon (tio ĉi estas nomata problemo de horizonto).

Kontraŭ tio la dedukta pruvo estas la jena: Se m estas nepara nombro, m - 1 estas para nombro, do ekzistas natura nombro k tia, ke m - 1 = 2 · k. Anstataŭ k nome sufiĉas elekti (m − 1) / 2, kio estas natura nombro ĝuste danke al la pareco de m - 1. Do m = 2 · k + 1. Simile ni motivigos, ke por nepara n ekzistas natura nombro l, tiel ke n = 2 · l + 1. Tiam la produto m · n egalas al (2 · k + 1) · (2 · l + 1) = 4 · k · l + 2 · k + 2 · l + 1. Ĉar 4 · k · l + 2 · k + 2 · l estas evidente para, m · n estas nepara, kion ni volis pruvi. Nur nun ni povas esti centprocente certaj pri tio, ke la aserto validas. Se estas nome donitaj du neparaj nombroj, validas por ili ĉiu unuopa paŝo de la pruvo, kaj do ankaŭ ties fino.

Hipotezo de primaj duopoj

Pli detalaj informoj troveblas en artikolo Hipotezo de primaj duopoj.

La hipotezo de primaj duopoj estas ĝis nun nepruvita aserto el la tereno teorio de nombroj, laŭ kiu ekzistas senfine multe da primoj p tiaj, ke eĉ p + 2 estas primo. Duopo de tiaj nombroj (p, p + 2) nomiĝas prima duopo.

La plej granda ĝis nun konata prima duopo estas (2003663613 · 2 ¹⁹⁵⁰⁰⁰ − 1, 2003663613 · 2¹⁹⁵⁰⁰⁰ + 1) , ambaŭ nombroj de tiu ĉi duopo havas (en dekuma sistemo) 58 711 ciferojn. Malgraŭ tio ke estas konataj tiel ĉi grandaj ekzemploj de la primaj duopoj, ne eblas konsideri hipotezon kiel dedukte (matematike) pruvita, ĉar eblas, ke ia plua pli granda prima duopo jam neniam estos trovita - simple tial, ke ĝi ne ekzistas. Tamen oni supozas (kaj necese aldoni, ke ne nur pro la jen signita indukta pruvo), ke la aserto validas. Ties pruvo tiel restas unu el la plej elvokemaj problemoj de la nuntempa teorio de nombroj.

Teoremoj de Gödel kaj limoj de deduktaj metodoj

Pli detalaj informoj troveblas en artikolo Teoremoj de nekompleteco.

Laŭ la teoremo de Gödel pri nekompleteco ekzistas en ĉiu sufiĉe komplika (tiom, ke eblus paroli en ĝi pri naturaj nombroj) matematika teorio, kiu ne estas memkontraŭdira kaj kies aksiomojn eblas efektive elskribi, asertoj, kiujn en tiu ĉi teorio eblas nek pruvi nek rifuzi (la teorio estas tiel nomate nekompleta). Inter tiujn teoriojn apartenas ekzemple aritmetiko de Pean aŭ teorio de aroj de Zermelo-Fraenkel.

Tiuj ĉi teoremoj do diras, ke la dedukta maniero de pruvado estas en granda mezuro limigata. Eblas nome dedukte pruvi eĉ ne ĉiujn asertojn, kiuj validas pri tiel simpla kaj alirebla fako, kia estas naturaj nombroj.

Historia evoluo

Antikvo

Egiptio kaj Babilono

Parto de papiruso de Rhind – kolekto de 84 solvitaj taskoj devenantaj el periodo inter Meza imperio kaj Nova imperio en antikva Egiptio

De la antikvaj egiptoj kaj babilonanoj estas konservitaj neniaj matematikaj pruvoj en la hodiaŭa senco de la vorto. Konserviĝis multe da registroj kaptantaj solvon de diversaj konkretaj problemoj kaj taskoj. Estas konsiderite, ke tiuj ĉi problemoj estis jam tiom abstraktaj kaj tiuj ĉi solvoj tiel elegantaj, ke en ilia fono devis stari profunda kompreno de la donita tereno ensumiganta implicite pruvojn de ĝusteco de la uzataj metodoj..

Ĉinio

En Ĉinio en la 5-a jarcento a.K. ĝis 3-a jarcento a.K. krom praktika matematiko evoluis ankaŭ logiko. Al tiu dediĉis sin precipe lernejo de sekvantoj de filozofo Mo Ti, kies anoj okupiĝis pri teorio de ekkono, kaj ili logike pruvadis siajn asertojn. Unu el la plej signifaj sekvantoj de Mo Ti estis Kung-sun Lung vivanta en la unua duono de la tria jarcento antaŭ Kristo.

Sed la logika pruvo ne estis en Ĉinio plu evoluigata. La doktrino de Mo Ti estis nome dum regado de dinastio Han tute forŝovita fare de konfuceismo kaj pli postaj ĉinaj filozofoj jam neniam plu revenis al ĝi.

Grekio

La nocio de dedukta matematika pruvo havas sian devenon en antikva Grekio. Same kiel la tuta tiama matematiko ankaŭ la matematika pruvo estis tre mallarĝe kunigita kun geometrio. La plej malnovaj matematikaj pruvoj devenas ĝuste el tiu ĉi tempo - ili konserviĝis en dektriparta verkaro Elementoj de Eŭklido.

Registrado en platona koncepto de geometrio

La matematika pruvo, tiel kiel ni konas ĝin hodiaŭ, havas siajn komencojn en la greka geometrio evoluigata subinflue de la filozofio de Platono. Influitaj de tiu ĉi filozofio, tiamaj geometroj klopodis malkovri la mondon de geometriaj ideoj kaj observi la veron enhavitan en ĝi. En tiu ĉi koncepto la matematika pruvo en la hodiaŭa senco de la vorto ankoraŭ ne ekzistis. Unusola ebleco, kiel kun absoluta certeco konstati la veron pri la geometria mondo, estis rekte observi tiun ĉi veron - registri ĝin. Se iu geometro sukcesis ekregistri validecon ekzemple de teoremo de Pitagoro - t.e. por mallonga momento li vere ekvidis, ke la sumo de grandecoj de enhavoj de du kvadratoj super lateroj de ortangulo egalas al la enhavo de kvadrato super ĝia hipotenuzo, tio estis ĉiam nur por tempo, dum kiu daŭris lia koncentriĝo. Tuj kiam la atentemo malstreĉiĝis, la vidkapablo, per kiu li rigardis en la mondon de geometriaj ideoj, nebuliĝis kaj la registro estis perdita. Por ke li povu kiam ajn reaperi tiun ĉi registron kaj ankaŭ por ke la saman eblecon li donu ankaŭ al ceteraj matematikistoj, tia geometro poste verkis instrukcion, kiel oni progresu (t.e. en kiajn lokojn de la geometria mondo rigardi), por denove ekvidi la verecon de teoremo de Pitagoro. Tiaj ĉi instrukcioj, el kiuj poste (en aristotela koncepto de geometrio) evoluis geometriaj konstruoj, estis la plej malnovaj antaŭuloj de la matematikaj pruvoj.

La estiĝo de matematika pruvo

La platona koncepto de matematiko ne estis longtempe retenebla. Kiel nome okazis evoluo de geometrio, la nove registritaj veroj estis kaŝitaj senĉese pli profunde en la mondo de la geometriaj ideoj. Geometro, kiu volis registri la donitan veron, devis ĉiufoje investi grandan klopodon. Plie ĉe tiel pretendemaj registroj estis tre komplike retenadi la vidkapablon tute klara kaj neombrigita dum la tuta tempo de rigardado en la geometrian mondon. Tia ĉi registro estis poste atingita por nura ono de sekundo, antaŭ ol ĉio denove dissolviĝis en nebulan malcertecon, en kiu la geometro ne sciis, ĉu li vere ekvidis la donitan veron aŭ ĉu tio estis nur ŝajno. La pretendemo de registroj de pli komplikaj geometriaj veroj estis en certa mezuro donita ankaŭ per tio, ke kiam ajn la geometro volis uzi ekzemple teoremon de Pitagoro, li devis ĝin unue denove reregistri en la donita konkreta kazo. Pro tiuj ĉi motivoj kelkaj geometroj rezignis (verŝajne eĉ ne konsciinte tion) de la platona maniero de rigardado en la mondon de ideoj kaj malrapide ili ekspiris al paŝo, kiu donis karakteron al la tuta matematiko ekde ilia tempo ĝis la nuntempo. Tiu ĉi paŝo estis enlaso de prudento en la mondon de matematiko. Se nome la geometro jam multfoje registris la teoremon de Pitagoro, li povis esti tute certa pri ties vereco. Se li bezonis pli poste uzi ĝin por registri alian veron, li konsciis, ke ne estas bezone denove reregistri ĝin en tiu ĉi konkreta kazo. Sufiĉis, ke li sciis pri ĝia valideco kaj same li sciis, ke se li nun registrus ĝin, li povus jam registri ankaŭ la veron, pri kiu temis al li. Tiu ĉi prudenta konsidero do anstataŭis la sinsekvon de registroj. Tio estis anstataŭo neokulfrapa - kiam ajn la geometro nome dezirus, li povus esti certa, ke surbaze de tiu ĉi konsidero li reregistrus la donitan veron. Sed spite al tiu ĉi neokulfrapeco temis pri principa paŝo. La geometriaj veroj jam ne bezonis esti sole registritaj, sufiĉis prudente motivigi, ke (kiam ajn iu deziros tion) ili povus esti registritaj. Tiel ĉi naskiĝis la matematika pruvo.

Oksirinĥa papiruso devenanta el la jaroj 75 – 125. Estas sur ĝi kaptita pruvo n-ro kvin el la dua libro Elementoj de Eŭklido.

Influo de Aristotelo

La signifo de Aristotelo por la tuta tiama kaj estonta eŭropa scienco estas grandega. La daŭraj kaj neŝanĝiĝemaj geometriaj ideoj estis sub lia influo anstataŭitaj per nuraj imagoj de geometriaj objektoj. Matematiko (eĉ tiutempe senĉese ankoraŭ reprezentata preskaŭ ekskluzive de geometrio) praktikata en ligiteco de la filozofio kaj logiko de Aristotelo konis jam logikan pruvon kiel konsideron okazanta en la lingvo, tio signifas simpla de kiaj ajn registroj (ĉar ideoj, kiujn ununurajn eblas registri, jam ne estis en la mondo de matematiko).

Grava karaktero de la pruvo komencas esti tiutempe lia rilato al veraj (komprenu imageblaj) objektoj. Tiun ĉi konekson eblas plej bone esprimi en rilato de sendisputeco kaj efektiveco. La sendisputeblaj estas tiaj pensitaj objektoj, el kies ecoj ne eblas dedukti logikan disputon (t.e. ne eblas pruvi ian econ kaj samtempe ties logikan neon). Realigeblaj estas male tiaj objektoj, kiujn eblas (almenaŭ en imago) realigi. La baza logika regulo difinita de Aristotelo diras, ke neia objekto povas havi samtempe econ kaj ankaŭ ties logikan neon. Do la pensita objekto, kiu estas disputa, ne povas esti realigebla. La mala aserto, t.e. sendisputebla objekto estas realigebla, tiutempe ne estis agnoskata kiel vera Ekzemple kvar reciproke ortaj segmentoj ja ne estas komune en disputo, sed pro limigo donita de tridimensia spaco ne eblas ilin realigi nek imagi.

Tiutempe ankaŭ kristaliĝis bazaj specoj de pruvmetodoj konataj kiel klasikaj modeloj de logikaj pruvoj Inter tiujn ĉi modeloj apartenas rekta pruvo, nerekta pruvo, pruvo de analizo de kazoj kaj pruvo de pensita konstruo (vidu sekcion pri Specoj de matematikaj pruvoj).

La aristotela koncepto de matematiko kaj matematika pruvo estas kaptita en verkoj Elementoj de Eŭklido, en kiuj ankaŭ unuafoje aperas ideo de aksioma konstruo de matematiko en formo de postulatoj de Eŭklido.

Romio

Romia matematiko ĝenerale estis neniam evoluigita kaj fakte ĝi restadis sur tiu nivelo de konoj, sur kiu postlasis ĝin grekoj. Pragmatika romia socio agnoskis sole tiun parton de matematiko, kiu taŭgis por aplikadoj en konstruaferoj kaj armeaferoj. Intereso pri la pura matematiko inkluzive de nocio de la matematika pruvo estis fakte nula.

Mezepoko

Paĝo el libro Hisáb al-ĝabr wa-l-muqábala

Matematiko kiel tutaĵo precipe en frua mezepoko spertis periodon de mallumo. La greka koncepto de matematiko kaj pruvoj estis plu praktikata sole en Bizanca imperio. De tie ekde la 8-a jarcento araboj interkonatiĝis kun tiu koncepto (grandan influon al la araba matematiko havis ankaŭ matematiko barata). La araba matematiko plenforte montriĝis en Hisáb al-ĝabr wa-l-muqábala (حساب الجبر و المقابلة‎), la verko de Al-Ĥorezmi, en kiu estis metitaj bazoj de algebro kaj kun tio koneksanta nova speco de la matematika pruvo - pruvo per kalkulo. Tiu ĉi nova speco de pruvo estis uzata ankaŭ pli poste fare de italaj renesancaj matematikistoj dum serĉado de ĝeneralaj solvoj de algebraj ekvacioj.

Novepoko

Konstruiga antaŭbolzana koncepto

Por koncepto de la matematika pruvo en Eŭropo en periodo ekde la 16-a ĝis la unua duono de la 19-a jarcento estas principa la nocio de fako, sur kiu tiama matematiko estis fondita. La fako estas tia limigo de certa klaso de efektivigeblaj objektoj, ke pri ĉiu objekto eblas decidi (almenaŭ teorie), ĉu ĝi apartenas en tiun ĉi fakon aŭ ne. Ekzemploj de la fakoj povas esti fakoj de naturaj nombroj, derivigeblaj realaj funkcioj, sed ankaŭ tiaj, ĉe kiuj ne estas konate, kiel ili precize aspektas aŭ ĉu ili ne estas eĉ malplenaj, kiel ekzemple fako de ĉiuj primaj duopoj pli grandaj ol 10^1 000 000.

Tiutempe estis en la matematiko senĉese karakterize evidenta influo de Aristotelo - la matematikaj objektoj ne havis daŭran ekzistadon kiel platonaj ideoj, sole eblis imagi ilin aŭ pensi ilin (efektivigi ilin en la imago respektive en la pensado). Tiuj ĉi objektoj akiradis en la efektivado sian ekzistadon, post la malstreĉiĝo de la atentemo ili ĉesis denove ekzisti. La fako do ne estis konsiderata kiel ia dosiero de daŭre ekzistantaj objektoj, sed kiel certa markigo de tiuj objektoj - la ekzistantaj, jam pereintaj, ĝis nun ne kreitaj kaj tiaj, kiuj neniam ekzistos - kiuj apartenas en tiun ĉi fakon (kaj due ankaŭ de tiuj, kiuj ne apartenas en ĝin). La pruvo de aserto "Por ĉiu objekto el la donita fako validas..." do ĉisence signifis la pruvadon de tiu ĉi aserto por ĉiu objekto (eĉ por tia, kiu estos neniam efektivigita) de tiu ĉi fako. Tiu ĉi koncepto kongruas kun la nuntempa komprenado de vortoj "por ĉiu". Diference de tio la frazo "Ekzistas objekto el la donita fako, ke validas..." ne estas en tiu ĉi koncepto aserto. Ties valideco nome ne estas daŭra, ĉar en la fako tiel, kiel ĝi estis ĉi tie eksplicita, la certa objekto ekzistas ĝuste tiam, kiam ĝi estas efektivigita en la pensado de iu homo. Tuj kiam la penso pereos, tia objekto ĉesas ekzisti, kaj do la valideco de tiu ĉi frazo povas dumtempe ŝanĝiĝi. Por ke akiru aserton, ni devas agadi pli atenteme kaj formuli la sekvantan frazon jene: "Temas pri efektivigebla objekto el la donita fako, ke validas..." Tian aserton poste eblas pruvi sole per unu maniero, kaj nome, ke la postulata objekto efektiviĝos - ekkonstruos sin. Ununura maniero de la pruvado de ekzistaj asertoj do estis ĉitempe pruvo per konstruigo. Pure ekzistiga, nekonstruiga pruvo el la pli menciitaj kaŭzoj ne estis uzata kaj ĝi nek povis. Krom la konstruiga pruvo kiel la ĝusta estis senĉese ankoraŭ konsiderata ankaŭ pruvo apogita je geometria opinio, sen kiu matematikistoj tiam ĉe certaj asertoj (ekz. ĉe teoremo de Bolzano) ne evitis.

Laŭ Bolzano, Dio estas diference de homo kapabla vidi ĉiujn senfine multajn elementojn de koŝia vico en unu fojo, kaj do li rekte registras eĉ punkton sur rektlinio, al kiu la elementoj de tiu ĉi vico proksimiĝas. Tia punkto do ekzistas, kvankam neniu homo kapablas konstrui ĝin.
_{(La reguligita bildo de William Blake The ancient of days)}

Influo de Bolzano kaj la nekonstruiga pruvo

La signifo de ĉeĥa filozofo kaj matematikisto Bernard Bolzano por la evoluo de ne nur koncepto de la matematika pruvo, sed kiel de la tuta matematiko konsistas en anstataŭo de fakoj per la daŭre ekzistantaj grupiĝoj de objektoj. El tiuj ĉi grupiĝoj pli poste evoluis la nocio de aro, kiu fariĝis la centra nocio de la matematiko de la 20-a jarcento. Ni notu rande, ke dum la anstataŭo de senfinaj fakoj per la grupiĝoj Bolzano devis solvi problemon de aktuala senfineco (t.e. problemon, ĉu reale ekzistas senfina kvanto de iaj objektoj). Li kapablis solvi tiun ĉi problemon sole helpe de teologio, kiam li motivigis, ke aktuale senfina kvanto troviĝas en menso de kristana Dio.

Se estas donitaj daŭre ekzistantaj grupiĝoj de objektoj, la frazo "Ekzistas objekto el la donita grupiĝo, ke validas..." havas jam (diference de ambaŭ kazoj) daŭran karakteron kaj ĝi do estas aserto. Tiun ĉi aserton poste eblas pruvi per du manieroj. La unua ebleco estas agadi same, kiel ĉe la kazo de la fakoj, t.e. ekkonstrui la postulatan objekton. Nova ebleco, kiu nun proponiĝas, estas pruvi nuran ekzistadon de la postulata objekto sen neceseco konstrui ian tian objekton. Tiu ĉi nova speco de pruvo nomiĝas nekonstruiga pruvo (aŭ pure ekzista pruvo). Tipa ekzemplo de uzo de la nekonstruiga pruvo estas la pruvo de ekzistado de transcenda nombro de Cantor, dum kiu montriĝos, ke de ĉiuj algebraj nombroj estas sole kalkuleble multe (eblas numeri ilin per naturaj nombroj), dum de ĉiuj realaj nombroj estas nekalkuleble multe (ne eblas numeri ilin). Ĉar do da realaj nombroj estas pli ol da algebraj, devas almenaŭ unu transcenda ekzisti. Sed el tiu ĉi pruvo entute ne estas tute klare, kiel trovi ian transcedentan nombron.

Ni aldonu, ke jam kelkaj antaŭaj filozofoj kaj teologoj (Giordano Bruno, Rodrigo de Arriaga) motivigis per uzo de supozo de Dia ekzistado, ke objektoj, kiuj reciproke ne estas en logika disputo jam devas esti efektivigeblaj (nome en Dia menso). Tiu ĉi aserto, kiu estas returno de la klasika percepto de Aristotelo pri neefektivigebleco de disputa, pli poste eksidis en la matematiko. Ties formaligo en parolo de la moderna matematika logiko estas la t.n. teoremo de Gödel pri kompleteco.

La estiĝo de formala pruvo

Sekve de la laboro de Bolzano venis en la terenon de esplorado de matematiko ankaŭ tiaj objektoj, kies ekzistado estas ja pruvebla, sed eblas ilin neniel ekkonstrui. Ekzemplo de tia objekto estas ekzemplo kontinua funkcio, kiu havas en nenia sia punkto derivaĵon (tangenton al grafo), malkovrita sendepende unue de Bolzano kaj pli poste de Weierstrass. Iom necerte dirite, la grafon de tia funkcio eblas desegni per unu movo, sed en ĉiu punkto de tiu ĉi grafo estas rompo, t.e. ne "glata arketo", sed "pinto". Ankoraŭ pli stranga ekzemplo povas esti kurblinio de Pean, kio estas simpla kontinua kurblinio difinita en intervalo (0,1), kies bildon plenigas la tuta kvadrato (0,1) x )0,1) aŭ funkcio el realaj en realajn nombrojn. Tiuj ĉi kaj al ili similaj ekzemploj tute kontraŭas al homa intuicio - Charles Hermite eĉ proklamis pri la funkcio de Bolzano-Weierstrass kaj pluaj similaj ekzemploj: "Mi forturnas min kun terurego kaj teruro de tiu ĉi bedaŭrinda inundo de kontinuaj funkcioj sen derivaĵo.". Sed pli principa por plua evoluo de la matematika pruvo estas reago de Henri Poincaré, kiu en verko La valeur de la Science demandas "Kiel intuicio povas ĉikaze tiel trompi nin?"

La miro de Poincaré estas komprenebla, ĉar pro la malkovro de pli supre menciitaj ekzemploj okazis io, kio ĝis tiutempo ne havis en la matematiko analogion. La geometria opinio kaj intucio venis en disputon kontraŭ pruveblaj asertoj. Tial, por ke oni malebligu la disputeblecon de la tuta matematiko, estis necese rifuzi la intuicion kaj la opinion kiel pruvigaj rimedoj. Sed la pruvoj de multaj bazaj asertoj precipe de matematika analizo kaj geometrio estis tiutempe fonditaj en la opinio, estis do devige konstrui ilin denove sur firman fundamenton. Tiu ĉi firma fundamento fariĝis aksioma metodo uzata jam en antikva Grekio fare de Eŭklido en liaj Elementoj. Sed ankaŭ Eŭklido eliris (verŝajne eĉ ne konsciinte tion) grandmezure el intuicio - pri tio atestas ekzemple fakto, ke dume da postulatoj de Eŭklido estas sole kvin, David Hilbert en sia laboro Grundlagen der Geometrie uzas al aksiomigo de geometrio 21 postulatojn. Ankaŭ greka aksiomiga metodo do montriĝis kiel nesufiĉa kaj antaŭ ol povis esti fondita sur ĝi la tuta matematiko, ĝi devis esti tute liberigita de la intuicio.

La loko, kie en la greka koncepto la intuicio estis uzata plej ofte, estis la matematika pruvo. Kvankam en la geometrio estis elektataj kiel la aksiomoj eĉ multaj el la plej evidentaj veroj, por ke oni tiel limigu la uzon de opinio al minimumo, la maniero de logika derivado de sekvoj mem estis uzata tute libere. Por ke oni tute eliminu la intuicion (kaj per tio ankaŭ la tutan necertecon) el la matematiko, devis do la matematikistoj de la dua duono de la 19-a jarcento aksiomigi la nocion de la matematika pruvo mem. Samtempe kun tio okazis sekve de klopodo pri forigo de neprecizeco eliranta el (intuicia) uzado de natura lingvo al formaligo de tiu ĉi nocio, t.e. anstataŭo de la natura lingvo per lingvo simbola. En laboroj de David Hilbert, Gottlob Frege kaj pluaj estis iom post iom evoluigita formala simbola lingvo sufiĉe riĉa, por ke ĝi esprimu ĉiujn matematikajn asertojn, kaj la nocio de formala pruvo, kiu ebligis pruvi formale skribitajn asertojn (la t.n. formulo) per uzo sole de kelke da malmulte da derivigaj reguloj, ni nomas logikaj aksiomoj, t.e. sen la plej malgranda influo de intuicio aŭ opinio. La matematika pruvo tiel fariĝis klare difinebla nocio tiom preciza, ke post veno de moderna komputila tekniko povis esti ties ĝusteco verkontrolita eĉ per nure algoritme laboranta komputilo.

Komputila pruvado

La historia evoluo alkondukis la matematikan pruvon en tian stadion de precizeco, ke ĝia ĝusteco povas esti verkontrolita per nura komputilo. Nuntempe eĉ ekzistas la t.n. sistemoj de aŭtomata pruvado de teoremoj, kio estas komputilaj programoj kapablaj ekkonstrui pruvojn de la matematikaj asertoj. Tiuj ĉi programoj ja multfoje kapablas pruvi eĉ ne tute trivialajn teoremojn, sed malgraŭ tio ili estas senĉese malproksime de la stadio, kiam eblus uzi ili en la praktiko. Inter faka matematika publiko ne ekzistas unusignifa opinio por tio, ĉu eblas evoluigi programon, kiu povus en la matematika pruvado konkursi kontraŭ homo.

Plua maniero de enigo de komputiloj en terenon de la pruvado estas pruvoj gvidataj fare de homo, sed en kiuj la komputilo estas uzita kiel helpanto en tiuj lokoj de la pruvo, kie oni bezonas nek inventon nek abstraktan pensadon. La plej konata tia uzo de komputilo estas pruvo pri teoremo kun kvar koloroj (vidu pli malsupren).

Ni notu, ke eblas pruvi la matematikajn teoremojn, laŭ kiuj povas ekzisti nenia komputila programo, kiu kapablus decidi pri ĉiu aserto, ĉu ĝi estas aŭ ne estas pruvebla (vidu decideblo).

Specoj de matematikaj pruvoj

La matematika pruvo estadas kutime farata (formultata) en natura lingvo, ĉiokaze nomata ankaŭ metalingvo. Tiu ĉi uzado de natura lingvo, kiu estas multfoje multsignifa, sed ĝi kondukas (precipe dum nesperteco de ties uzanto) al neprecizecoj kaj eraroj. La uzado de natura lingvo kondukas ankaŭ al multaj paradoksoj (vidu paradokso de Russell, paradokso de kretano aŭ paradokso de cent vortoj). Pruvo farata en la natura lingvo nomiĝas neformala pruvo. Klopodo al forigo de la neprecizecoj donitaj per la uzado de natura lingvo kondukis fine de la 19-a jarcento kaj komence de la 20-a jarcento al estiĝo de matematika logiko kaj al kreigo de nocio formala pruvo, en kiu la uzado de natura lingvo estas tute forigita (ĝi estas anstataŭita pere de formala lingvo). Sed pro pretendemo (precipe tempa) de konstruigado de formalaj pruvoj ankaŭ en la nuntempa matematiko unusignife dominas la pruvo neformala, kies mankoj kutime ĉe la sperta uzanto (matematikisto) ne estas fonto de eraroj.

Neformala pruvo

Neformala pruvo estas pruvo en natura lingvo eliranta el donitaj supozoj kaj reguloj de prudento. El la historiaj motivoj diferenciĝas kelke da bazaj specoj (neformalaj) de pruvoj.

Rekta pruvo

Pli detalaj informoj troveblas en artikolo Rekta pruvo.

La rekta pruvo (latine modus ponens) estas agado, dum kiu la pruvata aserto estas derivita per rekta apliko de difinoj, supozoj kaj antaŭe pruvitaj asertoj, alie dirite ĝi estas derivita per metodo "se... poste..." aŭ "...do".

Nerekta pruvo

Pli detalaj informoj troveblas en artikolo Nerekta pruvo.

La nerekta pruvo (latine modus tollens) estas metodo servanta al pruvado de aserto de tipo "se A, poste B", dum kiu pruviĝos "se ne B, poste ne A". Ĝi mallarĝe rilatas al pruvo per disputo - ĉiu nerekta pruvo povas esti facile transgvidita al la pruvo per disputo.

Pruvo per disputo

Pli detalaj informoj troveblas en artikolo Pruvo per disputo.

La pruvo per disputo (latine reductio ad absurdum) baziĝas dum uzo de erara supozo, kiu estas tuj poste alkondukita al disputo (estas el ĝi derivita evidente malvera aserto). Se tiel okazos, estas pruvita malvalideco de la donita supozo kaj do valideco de ties malo. La pruvo per disputo havas proksime al nerekta pruvo - ĉiu nerekta pruvo povas esti facile transgvidita al pruvo per disputo.

Pruvo per indukto

Pli detalaj informoj troveblas en artikolo Pruvo per indukto.

La pruvo per indukto konsistas en pruvado de ia aserto de tipo "por ĉiuj objektoj de certa klaso validas..." per maniero, dum kiu la objektoj de la donita klaso dividiĝos en sukcedon kaj montriĝos pri ili:

1. (unua paŝo) Por ĉiuj objektoj el la unua subklaso validas...
2. (indukta paŝo) Se validas ... por ĉiuj objektoj el la antaŭaj subklasoj, poste validas... ankaŭ por ĉiuj objektoj el subklaso senpere sekvanta malantaŭ ili.

Ekzistas multe da specoj de pruvoj de induktoj:

• matematika indukto (ĉiuj subklasoj estas unuelementaj kaj sukcedo kalkulebla).
• transfinia indukto (ĉiuj subklasoj estas unuelementaj kaj sukcedo povas esti libervola kardinala nombro).
• certigita indukto
• indukto laŭ komplikeco

Pruvo per pensita konstruigo

Pli detalaj informoj troveblas en artikolo Pruvo per pensita konstruigo.

La pruvo per pensita konstruigo estas metodo de pruvado de ekzistaj asertoj "ekzistas X tia, ke...", dum kiu oni konstruigos (ekkonstruos) objekton X, por kiu ... validas. Tiu ĉi speco de la pruvo ankaŭ iam estas nomata pruvo per indiko de ekzemplo.

Pruvo per analizo de kazoj

Pli detalaj informoj troveblas en artikolo Pruvo per analizo de kazoj.

Dum la pruvo per analizo de kazoj okazas dividigo de la esplorata situacio en fine multe da kazoj kaj pruvado de la postulata aserto por ĉiu el tiuj ĉi kazoj aparte. Tipa ekzemplo estas geometriaj pruvoj, kie ekzemple por valideco de ĝenerala teoremo pri triangulo oni konsideras tri kazojn de triangulo akutangula, ortangula kaj obtuza aŭ pruvoj, en kiuj diferenciĝas kazoj, kiam la donita nombro estas pozitiva, nula aŭ negativa.

Nekonstruiga (ekzista) pruvo

Pli detalaj informoj troveblas en artikolo Nekonstruiga pruvo.

La nekonstruiga pruvo de ia ekzista aserto "ekzistas X tia, ke..." estas tia pruvo, kiu ja pruvos la ekzistadon de tia X, sed eblas per nenia maniero aperigi el ĝi nek unusolan ekzemplon de objekto, kiu povus esti elektita anstataŭ X. Tiu ĉi speco de pruvo hodiaŭ estas jam plimulte agnoskata kiel ĝusta, sed en la pasinteco (precipe je interŝanĝo de la 19-a kaj la 20-a jarcento) multaj signifaj matematikistoj protestis kontraŭ tia ĉi maniero de pruvado kaj la asertojn pruvitaj per tiu ĉi maniero ili ne agnoskis. Nuntempe ekzistas en la matematiko memstara direkto la t.n. konstruismo, kiu klopodas pruvadi ĉiujn asertojn konstruktive (vidu intuicia logiko). Pioniroj sur kampo de nekonstruigaj pruvoj estis Georg Cantor (kun pruvo de ekzistado transcendaj nombroj) kaj precipe David Hilbert. La problemaro de nekonstruigaj pruvoj mallarĝe koneksas kun aksiomo de elekto kaj ekzistado (sendisputebleco) de aktuala senfineco.

Geometria pruvo

Pli detalaj informoj troveblas en artikolo Geometria pruvo.

Geometria pruvo de teoremo de Pitagoro

La geometria pruvo estas tia pruvo, kiu uzas metodojn de geometrio. Ties ilustriteco estas grandmezure donita per ebleco de geometria imago, sed la preciza geometria pruvo ne devas esti fondita en tia ĉi opinio. La geometriaj pruvoj estas plej ofte uzataj en la geometrio mem, sed tre ofte ankaŭ en matematika analizo kaj en teorio de nombroj.

Pruvo per kalkulo

Pli detalaj informoj troveblas en artikolo Pruvo per kalkulo.

Pruvo per kalkulo – sinsekvo de egalecoj plenigita per vorta komentario devenanta el libro de Gabriel Cramer Introduction a l’analyse de lignes courbes algébriques

La pruvo per kalkulo servas al pruvado de asertoj, kiuj havas formon de egaleco, neegaleco aŭ ian sistemon de antaŭaj du. Al la postulata rezulto oni venas el supozoj per kalkulo, t.e. per ripeta aplikado de bazaj aritmetikaj kaj algebraj reguloj kaj diversaj taksoj. La unuaj pruvoj per kalkulo aperis dum solvado de algebraj ekvacioj en verko de persa matematikisto Al-Ĥorezmi. Nuntempe la pruvo per kalkulo estas plej multe validigata en matematika analizo, lineara algebro, teorio de verŝajneco, numera matematiko kaj parencaj fakoj, kie tiu ĉi agado kreas ĉefan parton de la pruvoj de multaj asertoj. Sed ĝi estas malgrandmezure uzata eble en ĉiuj matematikaj disciplinoj escepte de geometrio.

Formala pruvo

Pli detalaj informoj troveblas en artikolo Formala pruvo.

La formala pruvo estas tia pruvo, kiu ne estas farata en la natura lingvo, sed en lingvo simbola - formala. Pro minimaligo de valoro de precizeco, kiu estadas ĉe ne neformala pruvo alta, por celoj de la formala pruvo estas komprenataj ĉiuj asertoj kiel fina sukcedo de signoj (la t.n. formulo, eventuale segmentoj) kaj estas enpraktigita sistemo de reguloj difinanta, kiel eblas manipuli kun tiuj ĉi sukcedoj. Tiu ĉi sistemo de reguloj nomiĝas logika kalkulo. Du la plej uzataj kalkuloj estas hilberta kalkulo kaj gentzena kalkulo. Ĉiu el tiuj ĉi kalkuloj konsistas el logikaj aksiomoj, kiuj esprimas bazajn ecojn de logikaj kunigiloj kaj kvantifikatoroj, kaj el derivigaj reguloj, kiuj difinas, per kia maniero eblas derivi el la supozoj iliajn sekvojn.

Kalkulo de Hilbert

Pli detalaj informoj troveblas en artikolo Kalkulo de Hilbert.

Formala pruvo en la hilberta kalkulo estas difinita kiel fina sukcedo de formuloj, el kiuj unu, kutime la lasta, esprimas la pruvatan aserton, kaj kies ĉiu membro estas aŭ

• logika aksiomo
• propra aksiomo de teorio, en kiu ĝi estas pruvata
• derivita el antaŭaj membroj laŭ unu el la derivigaj reguloj.

Kalkulo de Gentzen

Pli detalaj informoj troveblas en artikolo Kalkulo de Gentzen.

La gentzena kalkulo diferenciĝas de la hilberta ankaŭ per tio, ke ne estas pruvataj formuloj, sed la t.n. sekventoj, kio estas simboloj de formo $<A\Rightarrow B>$, kie $A$, $B$ estas finaj aroj de formuloj. Simbolo $<A\Rightarrow B>$ havas signifon "Se validas ĉiuj formuloj el A, poste validas almenaŭ unu formulo el B". Kiel pruvo de formulo $\varphi$ estas konsiderata la pruvo de sekvento $<\emptyset \Rightarrow \{\varphi \}>$.

Famaj historiaj pruvoj

Granda teoremo de Fermat

Pli detalaj informoj troveblas en artikolo Granda teoremo de Fermat.

Granda teoremo de Fermat estas la jena aserto:

Ne ekzistas pozitivaj entjeroj x, y, kaj z tiaj, ke validas xⁿ + yⁿ = zⁿ, por ia natura nombro n pli granda ol 2.

Tiu ĉi aserto estas unu el la plej famaj frazoj en la tuta historio de matematiko. La historio de pruvo de tiu ĉi frazo tuŝas ekde la mezepokaj arabaj matematiksitoj ĝis la fino de la 20-a jarcento mem kaj eblas sen troigado diri, ke provoj pri ties pruvo regula kaj karakterize influis la evoluon de la tuta matematika scienco, precipe de algebro kaj algebra teorio de nombroj

Pruvoj de la plej diversaj specialaj kazoj

Verŝajne jam mezepokaj arabaj matematikistoj sciis pri valideco de granda teoremo de Fermat por la kazo n = 3, sed iliaj pruvoj ne konserviĝis. La plej malnova konservita pruvo por tiu ĉi kazo devenas de Leonhard Euler.

Pierre de Fermat mem pruvis kazon la n = 4 tiel, ke por ĉiu eventuala solvo de tiu ĉi ekvacio li konstruis solvon pli malgrandan. Per tio li akiris senfinan malkreskantan vicon de naturaj nombroj kaj do disputon.

En la jaro 1825 Peter Dirichlet kaj Adrien-Marie Legendre sukcese solvis kazon n = 5 kaj en 1839 Gabriel Lamé n = 7.

En la jaro 1847 Ernst Kummer pruvis la teoremon de Fermat por ĉiuj regulaj primoj, inter kiuj apartenas primoj pli malgrandaj ol 100 escepte de 2, 37, 59 kaj 67.

Ĝenerala pruvo de Wiles

Andrew Wiles

Ĝeneralan kazon de granda teoremo de Fermat pruvis en la jaro 1995 Andrew Wiles post tio, kiam estis en lia supozita pruvo el la jaro 1993 trovita eraro. La pruvo de granda teoremo de Fermat estas escepta en multaj rilatoj. Ties longeco estas pli ol 100 paĝoj de presita teksto, ĝi estiĝis pro senĉesa naŭjara laboro de unusola matematikisto, sed ĉefe ĝi kunigas en si multajn diversajn iam eĉ sufiĉe malproksimaj terenojn de matematiko - teorion de diofantaj ekvacioj, modulara formo, algebra geometrio, galoja teorio kaj pluaj. Danke al tio ĝi estadas konsiderata kiel signifa paŝo direkte al plenigo de la t.n. programo de Langlands de ligigo de teorio de nombroj kaj de teorio de reprezentoj. Samtempe ĝi estas eminenta modelo de tio, kiel komplika povas esti la pruvo de simple formulita aserto.

Teoremo kun kvar koloroj

Pli detalaj informoj troveblas en artikolo Teoremo kun kvar koloroj.

La teoremo kun kvar koloroj diras, ke ĉiun mapon en ebenaĵo eblas kolorigi maksimume per kvar koloroj tiel, por ke ĉiuj du najbaraj teritorioj havu diferencan koloron. Konjekton, ke tio estas tiel, elparolis jam en la jaro 1852 juna matematikisto Francis Guthrie. En la jaro 1878 tiu ĉi konjekto ĝenerale interkonatiĝis, kiam Arthur Cayley postulis ĉiujn partoprenantojn de renkontiĝo de Londona matematika socio, por ke ili provu pruvi ĝin. Sed la konjekto rezistis al ĉiuj klopodoj pri la pruvo ankoraŭ pluajn preskaŭ cent jarojn. Nur en la jaro 1976 Kenneth Appel kaj Wolfgang Haken anoncis, ke ili trovis la pruvon.

Ekzemplo de mapo en ebenaĵo kolorigita per kvar koloroj.

La pruvo de Appel kaj Haken

Appel kaj Haken sukcesis redukti la tutan problemon de kvar koloroj al nuraj fine multe da kazoj, kiujn necesis solvi. Sed de tiuj kazoj estis tiom (precize 1936), ke pro ilia permana verkontrolado unu homo povus pasigi la tutan sian vivon eĉ ne solvinte ĉiujn. Tial la verkontrolado de tiuj ĉi kazoj estis komisiita al komputilo, kiu pasigis super ili pli ol 1200 horoj de maŝina tempo. Tiu ĉi uzo de komputilo por pruvi matematikan teoremon kaŭzis siatempe viglan polemikon. Neniu homo nome povis jam iam verkontroli la ĝustecon de la pruvo - eblis ja permane reverkontroli la ĝustecon de la komputila programo, kiu la unuopajn kazojn verkontrolis, sed tio ne eliminis eblecon de aparatara eraro, kiu povis la tutan pruvon malvalorigi. Por defendi la komputilan pruvadon estis argumentite, ke ĉe tiel komplikaj kaj longaj pruvoj la probableco de aparatara eraro estas ja nenula, sed certe multe malpli granda ol probableco, ke similan eraron faros homo Nuntempe la teoremo kun kvar koloroj estas konsiderata kiel pruvita kaj kontraŭ uzo de komputilo en la matematikaj pruvoj ne estas metataj pli grandaj obĵetoj.

Necesas aldoni, ke Appel kaj Haken kredis, ke ilia pruvo estas nur unua el vico, en kiuj komputiloj estos per principa maniero uzitaj . Sed la pruvo de la teoremo kun kvar koloroj restis en tiu ĉi ĝis la nuna tempo fakte sola kaj krom kelkaj pli-malpli trivialaj pruvoj rilatantaj al venkaj strategioj en kelkaj finaj ludoj ne estis jam denove en la matematika pruvado tiumaniere la komputilo uzita.

Klasifiko de finaj simplaj grupoj

Teoremo pri klasifiko de finaj simplaj grupoj diras, ke ĉiu fina simpla grupo falas aŭ en unun el 18 senfinaj grupoj aŭ ĝi estas unu el 26 tiel nomataj sporadaj grupoj. Tiu ĉi teoremo do plene karakterizas per tio ĉiujn finajn simplajn grupojn. Pro grandega pretendemo de ĝia pruvo ĝi estadas en la angla ankaŭ nomata "Enormous theorem".

Pruvo

Pruvo de tiu ĉi teoremo estis neniam publikigita en tuto. Ĝi konsistas el pli ol 500 artikoloj de proksimume 100 aŭtoroj publikigitaj en la plej diversaj matematikaj ĵurnaloj plejparte inter la jaroj 1955 kaj 1983. Oni taksas, ke la suma longeco de pruvo estas 10 000–15 000 paĝoj de presita teksto Tia amplekseco povas kaŭzi (simile kiel ĉe la teoremo kun kvar koloroj) dubojn pri la ĝusteco de la pruvo. Neniu matematikisto nome verŝajne tralegis tiun ĉi pruvon tuta, kaj do neniu en la mondo povas aserti mem pri si, ke ne estas eraro en ĝi. Sed ĉiu unuopa parto de la pruvo publikita en la paso de preskaŭ tridek jaroj estis fare de multaj matematikistoj tralegita kaj agnoskita kiel ĝusta. Tial tiu ĉi pruvo estas ĝenerale konsiderata kiel ĝusta, kvankam neniu konkreta homo iam verkontrolis ĝian ĝustecon kaj tre verŝajne eĉ ne en la estonteco verkontrolos.

Rilate al la nekredebla longeco de la pruvo estas alte verŝajne, ke ĝi enhavas multe da etaj eraroj kaj malĝustecoj. Michael Aschbacher, unu el la ĉefaj aŭtoroj de la pruvo, diris al tio: "Verŝajneco de eraro en la klasifika teoremo estas fakte 1. Aliflanke verŝajneco, ke ĉiu unu el tiuj ĉi eraroj ne estus facile korektebla, estas fakte nulo kaj ĉar la pruvo estas fina, la verŝajneco, ke la teoremo ne validas, estas tre proksime al nulo. Kiel la tempo pasas kaj ni havas okazon pli proksime interkonatiĝi kun la pruvo, nia fido en ĝi povas unusole kreski."

Rilataj temoj

• Historio de matematiko
• K.E.P.
• Pruvo (rajto)
• Teorio de pruvo
• Aksiomo
• Teoremo de Gödel pri nekompleteco

Eksteraj ligiloj

Literaturo

• Vítězslav Švejdar: Logika, neúplnost, složitost a nutnost. Praha: Academia, 2002. ISBN 80-200-1005-X.
• Petr Vopěnka: Rozpravy s geometrií. Praha: Panorama, 1989.
• Petr Vopěnka: Vyprávění o kráse novobarokní matematiky. Praha: Práh, 2004. ISBN 80-7252-103-9.

Rete angle

• The History and Concept of Mathematical proof (pdf) – artikolo pri la historio kaj filozofia principigo de la matematika pruvo
• Notes on methods of proof Arkivigite je 2017-06-02 per la retarkivo Wayback Machine – paĝoj enhavantaj priskribon de kelkaj la plej gravaj pruvaj metodoj
• Some mathematical proofs Arkivigite je 2007-04-29 per la retarkivo Wayback Machine – humura listo de kelke da ne ĝuste rigoraj, sed ofte uzataj pruvaj parolturnoj
• Coq a IMPS – du sistemoj de aŭtomata pruvado teoremoj libere al ludigo

Rete ĉeĥe

• Co je to (Fregovská) logika? (pdf) – mallonga artikolo de Jaroslav Peregrin ne nur pri la matematika pruvo en koncepto de Freg