Vidi fonton por Matematika pruvo

{{Jama ADLS}}
[[Dosiero:Euclid-proof.jpg|eta|Pruvo de aserto, ke ĉiu [[segmento]] estas flanko de iu [[egallatera triangulo]] , devenanta el [[bazo]]j 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 ([[aksiomo]]j).

La matematika pruvo devas esti eksplicite bazita sur nedubeblaj reguloj de [[Prudento|prudenta]] rezonado (tiaj reguloj estas esprimataj en [[matematika logiko]] en formo de [[aksiomo]]j 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.<ref name=100proof3>{{citu libron
  | last = Garnier
  | first = Rowan
  | authorlink = Rowan Garnier
  | title = 100% Mathematical Proof
  | publisher = John Wiley & Sons
  | series = 
  | year = 1996
  | doi = 
  | isbn = 0 471 96198 1 }} p. 3</ref>. La matematika pruvo estas nome diference de pruvoj en aliaj terenoj de homa farado (ekz. en [[juro]], [[naturscienco]] ktp.) almenaŭ principe nedubebla <ref name=100proof1>{{citu libron
  | last = Garnier
  | first = Rowan
  | authorlink = Rowan Garnier
  | title = 100% Mathematical Proof
  | publisher = John Wiley & Sons
  | series = 
  | year = 1996
  | doi = 
  | isbn = 0 471 96198 1 }} p. 1.</ref>. Ne estas eliminite, ke oni sukcesos matematike pruvi [[teoremo]]n, 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 ===
{{Ĉefartikolo|Indukta logiko|Dedukta logiko}}

==== Indukta pruvado ====
En ĉiuj [[scienco|sciencaj]] disciplinoj escepte de la matematiko la [[teorio]]j 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<ref name=100proof1/>.

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 [[Leĝoj de Newton pri movado#La dua leĝo de Newton pri movado: Fundamenta Leĝo de Dinamiko|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 jarcento]]j kelkaj eksperimentoj pruvis, ke la movo de lumo ne direktas sin per la [[Leĝoj de Newton pri movado|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 [[supozo]]j sole surbaze de de logikaj konsideroj. Plie tiuj ĉi logikaj konsideroj estas dividitaj en [[fina aro|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<ref name=Bourbaki1>{{citu libron
  | last = Bourbaki
  | first = Nicolas
  | authorlink = Nicolas Bourbaki
  | title = Elements of the History of Mathematics
  | publisher = Springer-Verlag
  | series = 
  | year = 1998
  | doi = 
  | isbn = 3-540-64767-8 }} p. 1.</ref>.

=== Ekzemploj de induktaj kaj deduktaj pruvoj de matematikaj asertoj ===
==== Produto de du neparaj nombroj estas nepara ====
Ni konsideru [[teoremo|aserton]]: "[[Produto]] de ĉiuj du [[Pareco de nombroj|neparaj]] [[natura nombro|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<sup>1 000 000</sup> (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 [[Pareco de nombroj|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 nombroj|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 ====
{{Ĉefartikolo|Hipotezo de primaj duopoj}}
La hipotezo de primaj duopoj estas ĝis [[nun en 2010|nun]] nepruvita aserto el la tereno [[teorio de nombroj]], laŭ kiu ekzistas senfine multe da [[primo]]j ''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 <sup>195000</sup> − 1, 2003663613 · 2<sup>195000</sup> + 1) <ref name=mathworld>{{citu libron
  | last = Weisstein
  | first = Eric W
  | authorlink = Eric Weisstein
  | title = Twin Primes
  | publisher = 
  | series = 
  | year = 2007
  | url = http://mathworld.wolfram.com/TwinPrimes.html
  | isbn =  }}</ref>, 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 [[hipotezo]]n 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<ref name=mathworld/>.

== Teoremoj de Gödel kaj limoj de deduktaj metodoj ==
{{Ĉefartikolo|Teoremoj de nekompleteco}}
Laŭ la [[Teoremoj de nekompleteco|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 [[aksiomo]]jn eblas efektive elskribi, asertoj, kiujn en tiu ĉi teorio eblas nek pruvi nek rifuzi (la teorio estas tiel nomate [[kompleta teorio|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 [[natura nombro|naturaj nombroj]].

== Historia evoluo ==
=== Antikvo ===
==== Egiptio kaj Babilono ====
[[Dosiero:Egyptian A'h-mosè or Rhind Papyrus (1065x1330).png|eta|Parto de [[papiruso de Rhind]] – kolekto de 84 solvitaj taskoj devenantaj el periodo inter [[Meza imperio]] kaj [[Nova imperio]] en [[antikva Egiptio]]]]
De la [[antikva Egiptio|antikvaj egiptoj]] kaj [[Babilono|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.<ref name=Bourbaki1/>.

==== Ĉ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.<ref>{{citu libron
  | last = Blundenová
  | first = Caroline
  | authorlink = Caroline Blundenová
  | title = Svět Číny
  | publisher = Knižní klub, Praha
  | series = 
  | year = 1997
  | url = 
  | isbn = 80-7176-420-5 }} p. 194</ref> 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]]<ref name=Bourbaki1/>. 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|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 [[ideo]]j 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 [[latero]]j 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 [[geometria konstruo|geometriaj konstruoj]], estis la plej malnovaj antaŭuloj de la matematikaj pruvoj.

===== La estiĝo de matematika pruvo =====
La [[Platono|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 [[teoremo de Pitagoro|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.
[[Dosiero:Oxyrhynchus papyrus with Euclid's Elements.jpg|eta|maldekstra|290px|[[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|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,<ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Rozpravy s geometrií
  | publisher = Panorama, Praha
  | series = 
  | year = 1989
  | url = 
  | isbn =  }} p. 219</ref> 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 [[logika disputo|logikan disputon]] (t.e. ne eblas pruvi ian econ kaj samtempe ties [[logika neo|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<ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Rozpravy s geometrií
  | publisher = Panorama, Praha
  | series = 
  | year = 1989
  | url = 
  | isbn =  }} p. 198-202.</ref> Ekzemple kvar reciproke [[ortanguleco|ortaj]] [[segmento]]j 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 <ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Rozpravy s geometrií
  | publisher = Panorama, Praha
  | series = 
  | year = 1989
  | url = 
  | isbn =  }} p. 223.</ref> Inter tiujn ĉi modeloj apartenas [[rekta pruvo]], [[nerekta pruvo]], [[pruvo de analizo de kazoj]] kaj [[pruvo de pensita konstruo]] (vidu sekcion pri [[Matematika pruvo#Specoj de matematikaj pruvoj|Specoj de matematikaj pruvoj]]).

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

==== Romio ====
[[Antikva Romio|Romia]] matematiko ĝenerale estis neniam evoluigita kaj fakte ĝi restadis sur tiu nivelo de konoj, sur kiu postlasis ĝin grekoj. [[Pragmatismo|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 ===
[[Dosiero:Image-Al-Kitāb al-muḫtaṣar fī ḥisāb al-ğabr wa-l-muqābala.jpg|eta|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 [[Barato|barata]]). La araba matematiko plenforte montriĝis en ''Hisáb al-ĝabr wa-l-muqábala'' ({{fremdlingve|ar|حساب الجبر و المقابلة}}), 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 [[renesanco|renesancaj]] matematikistoj dum serĉado de ĝeneralaj solvoj de [[algebra ekvacio|algebraj ekvacioj]].

=== Novepoko ===
==== Konstruiga antaŭbolzana koncepto ====
Por koncepto de la matematika pruvo en Eŭropo en periodo ekde la [[16-a jarcento|16-a]] ĝis la unua duono de la [[19-a jarcento]] estas principa la nocio de ''fako'', sur kiu tiama matematiko estis fondita.<ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Vyprávění o kráse novobarokní matematiky
  | publisher = Práh, Praha
  | series = 
  | year = 2004
  | url = 
  | isbn = 80-7252-103-9 }} p. 242.</ref> 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 [[natura nombro|naturaj nombroj]], [[derivaĵo (matematiko)|derivigeblaj]] realaj [[funkcio (matematiko)|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 [[hipotezo de primaj duopoj|primaj duopoj]] pli grandaj ol 10<sup>1&nbsp;000&nbsp;000</sup>.

Tiutempe estis en la matematiko senĉese karakterize evidenta influo de [[Aristotelo]] - la matematikaj objektoj ne havis daŭran ekzistadon kiel [[ideo|platonaj ideoj]], sole eblis [[imago|imagi]] ilin aŭ [[pensado|pensi]] ilin (efektivigi ilin en la imago respektive en la pensado). Tiuj ĉi objektoj akiradis en la efektivado sian [[ekzistado]]n, 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 [[teoremo|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 [[ekzista aserto|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.
[[Dosiero:God and Cauchy sequences.JPG|eta|maldekstra|250px|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.
<br />
<center>
<sub>(La reguligita bildo de [[William Blake]] ''The ancient of days'')</sub>
</center>]]

==== 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 [[kristanismo|kristana]] [[Dio]].<ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Vyprávění o kráse novobarokní matematiky
  | publisher = Práh, Praha
  | series = 
  | year = 2004
  | url = 
  | isbn = 80-7252-103-9 }} p. 170-177.</ref>

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 [[Georg Cantor|Cantor]], dum kiu montriĝos, ke de ĉiuj [[algebra nombro|algebraj nombroj]] estas sole [[kalkulebla aro|kalkuleble]] multe (eblas numeri ilin per naturaj nombroj), dum de ĉiuj [[reala nombro|realaj nombroj]] estas [[nekalkulebla aro|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).<ref>{{citu libron
  | last = Vopěnka
  | first = Petr
  | authorlink = Petr Vopěnka
  | title = Vyprávění o kráse novobarokní matematiky
  | publisher = Práh, Praha
  | series = 
  | year = 2004
  | url = 
  | isbn = 80-7252-103-9 }} p. 111-144.</ref> 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 de predika logiko|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ĵo]]n (tangenton al grafo), malkovrita sendepende unue de Bolzano kaj pli poste de [[Karl Weierstrass|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 funkcio|simpla]] kontinua [[kurblinio]] difinita en intervalo (0,1), kies bildon plenigas la tuta [[kvadrato]] (0,1) x )0,1) aŭ funkcio el [[reala nombro|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."''<ref name=Bourbaki15>{{citu libron
  | last = Bourbaki
  | first = Nicolas
  | authorlink = Nicolas Bourbaki
  | title = Elements of the History of Mathematics
  | publisher = Springer-Verlag
  | series = 
  | year = 1999
  | doi = 
  | isbn = 3-540-64767-8 }} p. 15.</ref>. 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?"''<ref name=Bourbaki15/>

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 de Eŭklido|Elementoj]]. Sed ankaŭ Eŭklido eliris (verŝajne eĉ ne konsciinte tion) grandmezure el intuicio - pri tio atestas ekzemple fakto, ke dume da [[postulato de Eŭklido|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 (logiko)|formulo]]) per uzo sole de kelke da malmulte da derivigaj reguloj, ni nomas [[logika aksiomo|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 [[algoritmo|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 [[komputila programo|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 [[Matematika pruvo#Teoremo kun kvar koloroj|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 [[decidebla teorio|decideblo]]).

== Specoj de matematikaj pruvoj ==
La matematika pruvo estadas kutime farata (formultata) en [[lingvo|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 [[antinomio de Russell|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 [[lingvo (logiko)|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 [[lingvo|natura lingvo]] eliranta el donitaj [[supozo]]j kaj reguloj de [[prudento]]. El la historiaj motivoj diferenciĝas kelke da bazaj specoj (neformalaj) de pruvoj.

==== Rekta pruvo ====
{{Ĉefartikolo|Rekta pruvo}}
La '''rekta pruvo''' (latine ''modus ponens'') estas agado, dum kiu la pruvata aserto estas derivita per rekta apliko de [[difino]]j, supozoj kaj antaŭe pruvitaj asertoj, alie dirite ĝi estas derivita per metodo "se... poste..." aŭ "...do".

==== Nerekta pruvo ====
{{Ĉefartikolo|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 ====
{{Ĉefartikolo|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 ====
{{Ĉefartikolo|Pruvo per indukto}}
La '''pruvo per indukto''' konsistas en pruvado de ia aserto de tipo "por ĉiuj objektoj de certa [[klaso (matematiko)|klaso]] validas..." per maniero, dum kiu la objektoj de la donita klaso dividiĝos en [[sukcedo]]n kaj montriĝos pri ili:
# (unua paŝo) Por ĉiuj objektoj el la unua subklaso validas...
# (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 aro|kalkulebla]]).
* [[transfinia indukto]] (ĉiuj subklasoj estas unuelementaj kaj sukcedo povas esti libervola [[kardinala nombro]]).
* [[certigita indukto]]
* [[indukto laŭ komplikeco]]

==== Pruvo per pensita konstruigo ====
{{Ĉefartikolo|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 ====
{{Ĉefartikolo|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 [[geometrio|geometriaj]] pruvoj, kie ekzemple por valideco de ĝenerala [[teoremo]] pri [[triangulo]] oni konsideras tri kazojn de triangulo [[akuta triangulo|akutangula]], [[Orta triangulo|ortangula]] kaj [[obtuza triangulo|obtuza]] aŭ pruvoj, en kiuj diferenciĝas kazoj, kiam la donita [[nombro]] estas pozitiva, nula aŭ negativa.

==== Nekonstruiga (ekzista) pruvo ====
{{Ĉefartikolo|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 jarcento|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 [[intuiciisma logiko]]). Pioniroj sur kampo de nekonstruigaj pruvoj estis [[Georg Cantor]] (kun pruvo de ekzistado [[transcenda nombro|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 ====
{{Ĉefartikolo|Geometria pruvo}}
[[Dosiero:Pythagorean proof.png|eta|maldekstra|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 ====
{{Ĉefartikolo|Pruvo per kalkulo}}
[[Dosiero:Gabriel Cramer- Introduction a l’analyse de lignes courbes algébriques - page 657.png|eta|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 (matematiko)|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 [[aritmetiko|aritmetikaj]] kaj [[algebro|algebraj]] reguloj kaj diversaj [[takso (matematiko)|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 ===
{{Ĉefartikolo|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 (logiko)|formulo]], eventuale [[segmento (gentzena kalkulo)|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 [[kalkulo de Hilbert|hilberta kalkulo]] kaj [[Kalkulo de Gentzen|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 ====
{{Ĉefartikolo|Kalkulo de Hilbert}}
Formala pruvo en la '''hilberta kalkulo''' estas difinita kiel fina [[sukcedo]] de [[formulo (logiko)|formuloj]], el kiuj unu, kutime la lasta, esprimas la pruvatan aserton, kaj kies ĉiu membro estas aŭ
* [[logika aksiomo]]
* propra [[aksiomo]] de [[teorio (logiko)|teorio]], en kiu ĝi estas pruvata
* derivita el antaŭaj membroj laŭ unu el la derivigaj reguloj.

==== Kalkulo de Gentzen ====
{{Ĉefartikolo|Kalkulo de Gentzen}}
La '''gentzena kalkulo''' diferenciĝas de la hilberta ankaŭ per tio, ke ne estas pruvataj formuloj, sed la t.n. [[sekvento (gentzena kalkulo)|sekventoj]], kio estas simboloj de formo <math><A \Rightarrow B></math>, kie <math>A</math>,&nbsp;<math>B</math> estas finaj aroj de [[formulo (logiko)|formuloj]]. Simbolo <math><A \Rightarrow B></math> havas signifon "Se validas ĉiuj formuloj el ''A'', poste validas almenaŭ unu formulo el ''B''". Kiel pruvo de formulo <math>\varphi</math> estas konsiderata la pruvo de sekvento <math><\emptyset \Rightarrow \{\varphi\}></math>.

== Famaj historiaj pruvoj ==
=== Granda teoremo de Fermat ===
{{Ĉefartikolo|Granda teoremo de Fermat}}
Granda teoremo de Fermat estas la jena aserto:
:''Ne ekzistas [[pozitiva nombro|pozitivaj]] [[entjero]]j x, y, kaj z tiaj, ke validas x<sup>n</sup> + y<sup>n</sup> = z<sup>n</sup>, por ia [[natura nombro]] n pli granda ol 2.''

Tiu ĉi [[aserto (matematiko)|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 [[mezepoko|mezepokaj]] [[araboj|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]]<ref>{{citu libron
  | last = Marcus
  | first = Daniel
  | authorlink = Daniel Marcus
  | title = Number Fields
  | publisher = Number Fields
  | year = 1977
  | isbn =  0-387-90279-1}} p. 6.</ref>

==== 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.<ref>{{citu libron
  | last = Cajori
  | first = Florian
  | authorlink = Florian Cajori
  | title = A History of Mathematics
  | publisher = AMS Chelsea Publishing
  | year = 
  | isbn = 0-8218-2102-4 }} p. 106.</ref> 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 [[pruvo per disputo|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 [[regula primo|regulaj primoj]], inter kiuj apartenas [[primo]]j pli malgrandaj ol 100 escepte de 2, 37, 59 kaj 67.

==== Ĝenerala pruvo de Wiles ====
[[Dosiero:Andrew wiles1-3.jpg|eta|[[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 [[diofanta ekvacio|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 ===
{{Ĉefartikolo|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.
[[Dosiero:Four Colour Map Example.svg|eta|maldekstra|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 [[aparataro|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<ref name=100proof10>{{citu libron
  | last = Garnier
  | first = Rowan
  | authorlink = Rowan Garnier
  | title = 100% Mathematical Proof
  | publisher = John Wiley & Sons
  | year = 1996
  | isbn = 0 471 96198 1 }} p. 10.</ref> 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 <ref name=100proof10/>. 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 [[teorio de ludoj|ludoj]] ne estis jam denove en la matematika pruvado tiumaniere la komputilo uzita.

=== Klasifiko de finaj simplaj grupoj ===
Teoremo pri klasifiko de finaj [[simpla grupo|simplaj grupoj]] diras, ke ĉiu fina simpla grupo falas aŭ en unun el 18 senfinaj grupoj aŭ ĝi estas unu el 26 tiel nomataj [[sporada grupo|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<ref name=100proof12>{{citu libron
  | last = Garnier
  | first = Rowan
  | authorlink = Rowan Garnier
  | title = 100% Mathematical Proof
  | publisher = John Wiley & Sons
  | year = 1996
  | isbn = 0 471 96198 1 }} p. 12.</ref> 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."''<ref name=100proof12/>

== Referencoj ==
{{Referencoj}}

== Rilataj temoj ==
* [[Historio de matematiko]]
* [[K.E.P.]]
* [[Pruvo (rajto)]]
* [[Pruvoteorio]]
* [[Aksiomo]]
* [[Teoremoj de nekompleteco|Teoremo de Gödel pri nekompleteco]]

{{Projektoj}}

== 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 ===
* [http://www.math.wustl.edu/~sk/eolss.pdf The History and Concept of Mathematical proof (pdf)] – artikolo pri la historio kaj filozofia principigo de la matematika pruvo
* [http://www.math.csusb.edu/notes/proofs/pfnot/pfnot.html Notes on methods of proof] {{Webarchiv|url=https://web.archive.org/web/20170602022904/http://www.math.csusb.edu/notes/proofs/pfnot/pfnot.html |date=2017-06-02 }} – paĝoj enhavantaj priskribon de kelkaj la plej gravaj pruvaj metodoj
* [http://paul.merton.ox.ac.uk/science/maths-proofs.html Some mathematical proofs] {{Webarchiv|url=https://web.archive.org/web/20070429081037/http://paul.merton.ox.ac.uk/science/maths-proofs.html |date=2007-04-29 }} – humura listo de kelke da ne ĝuste rigoraj, sed ofte uzataj pruvaj parolturnoj
* [http://coq.inria.fr/ Coq] a [http://imps.mcmaster.ca/ IMPS] – du sistemoj de aŭtomata pruvado teoremoj libere al ludigo

=== Rete ĉeĥe ===
* [http://jarda.peregrin.cz/mybibl/PDFTxt/412.pdf Co je to (Fregovská) logika? (pdf)] – mallonga artikolo de [[Jaroslav Peregrin]] ne nur pri la matematika pruvo en koncepto de Freg

{{Elstara}}

{{Havenda artikolo|Matematika pruvo}}

[[Kategorio:Pruvoj| ]]
[[Kategorio:Matematika logiko]]