Matematika pruvo

[eta|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 
#### 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.

### 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 101 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 
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 195000 − 1, 2003663613 · 2195000 + 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 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 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 
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 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 101&nbsp;000&nbsp;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.
[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.

(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 Peano, 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?"*

#### 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 
[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 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 
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.
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 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  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."*

## Referencoj 
## Rilataj temoj 
* Historio de matematiko
* K.E.P.
* Pruvo (rajto)
* Pruvoteorio
* 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  – paĝoj enhavantaj priskribon de kelkaj la plej gravaj pruvaj metodoj
* Some mathematical proofs  – 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


Kategorio:Matematika logiko