Prova assistida per ordenador

"Averiguar si qualsevol mapa es pot pintar en quatre colors, de manera que qualsevol parell de regions contigües estiguen pintades de diferents colors". En 1976, K. Appel i V. Haken, en l'ajuda de càlculs d'ordenador dissenyats a l'efecte, varen demostrar que és possible colorear qualsevol mapa en quatre colors

Una prova assistida per ordenador és una demostració matemàtica que ha segut generada a lo manco parcialment utilisant una computadora.

La majoria de les proves assistides per ordenador fins a la data han segut desenrolls de proves per exhaustación d'un elevat número de casos associats a un teorema matemàtic. L'idea és usar un programa de computadora per a realisar càlculs llarcs i proporcionar una prova de que el resultat d'estos càlculs implica la teorema donada. En 1976, el teorema dels quatre colors va ser la primera teorema important que es va verificar en un programa informàtic.

També s'han realisat intents en l'àrea d'investigació de l'inteligència artificial per a crear proves més menudes, explícites i noves de teoremes matemàtiques d'avall cap a dalt usant tècniques de raonament automàtic, com la busca heurística. Tals demostracions automàtiques de teoremes han demostrat numerosos nous resultats i han trobat noves proves per a teoremes conegudes. Ademés, la demostració interactiva de teoremes permet als matemàtics desenrollar proves llegibles per als sers humans que, no obstant, es verifiquen formalment per a verificar la seua exactitut. Ya que estes proves són generalment revisables pels matemàtics (encara que no sense dificultats, com en la prova de la conjectura de Robbins) no compartixen les implicacions controvertides de les proves assistides per ordenador per mig d'agotament.

Métodos

Un método per a usar computadores en proves matemàtiques és per mig dels sistemes denominats validació numèrica o rigor numèric. Açò significa calcular numèricament, pero en rigor matemàtic. S'usa de principis aritmètics i l'inclusió en valors establits per a garantisar que l'eixida de valor fix d'un programa numèric tanque la solució del problema matemàtic original. Açò es fa controlant, adjuntant i propagant els errors de grosseig i truncació usant, per eixemple, intervals aritmètics. Més precisament, si es reduïx el càlcul a una seqüència d'operacions elementals, com (+, -, *, /). En una computadora, el resultat de cada operació elemental es completa en la seua precisió de càlcul. No obstant, pot construir-se un interval proporcionat per llímits superiors i inferiors sobre el resultat d'una operació elemental. A continuació es procedix reemplaçant números per intervals i realisant operacions elementals entre dits intervals de números representables.

Objeccions filosòfiques

Artícul principal → Prova no prospectable.

Les proves assistides per ordenador són objecte de certa controvèrsia en el món de les matemàtiques, sent Thomas Tymoczko un dels primers en formular objeccions. Aquells que s'adherixen als arguments de Tymoczko creuen que les llargues proves assistides per ordenador no són, en cert sentit, demostracions reals perque impliquen tants passos llògics que no són pràcticament verificables pels sers humans, i que s'està demanant als matemàtics que reemplacen de forma efectiva la deducció llògica de axioma assumits per la confiança en un procés computacional empíric, que es veu potencialment afectat per errors en el programa de la computadora, aixina com també per defectes en l'entorn de temps d'eixecució i del propi dispositiu.

Atres matemàtics creuen que les llargues proves assistides per computadora deuen considerar-se com a càlculs, en lloc de proves: l'algoritme de prova en sí mateixa deu provar-se com a vàlit, de modo que el seu us pot considerar-se com una mera verificació. Els arguments de que les proves assistides per ordenador estan subjectes a errors en els seus programes font, compiladors i dispositius electrònics poden resoldre's proporcionant una prova formal de correcció del programa informàtic (un enfocament que es va aplicar en èxit a la teorema dels quatre colors en 2005), aixina com replicar el resultat usant diferents llenguages de programació, diferents compiladors i diferents tipos de computadora.

Una atra forma possible de verificar les proves assistides per ordenador és generar els seus passos de raonament en una forma llegible per una màquina, i després usar una demostració automàtica de teoremes per a comprovar la seua correcció. Este enfocament d'usar un programa de computadora per a provar que un atre programa és correcte no atrau als escèptics de les proves en ordenador, que ho veuen com una capa de complexitat afegida sense abordar la necessitat percebuda de la comprensió humana.

Un atre argument en contra de les proves assistides per ordenador és que carixen de bellea matemàtica, que no proporcionen idees ni conceptes nous i útils. De fet, est és un argument que podria alvançar-se contra qualsevol prova prolongada per agotament.

Una qüestió filosòfica adicional plantejada per les proves assistides per ordenador és si convertixen les matemàtiques en una ciència cuasi-empírica, en la que el método científic es torna més important que l'aplicació de la raó pura en l'àrea dels conceptes matemàtics abstractes. Açò es relaciona directament en l'argument dins de les matemàtiques sobre si les matemàtiques es basen en idees, o simplement són un eixercici de manipulació de símbols formals. També planteja la qüestió de si, d'acort en el punt de vista platònic, tots els objectes matemàtics possibles en algun sentit "ya existixen"; si les matemàtiques assistides per ordenador són una ciència observacional com l'astronomia, en lloc d'una experimental com la física o la química. Curiosament, esta controvèrsia dins de les matemàtiques està ocorrent al mateix temps que les preguntes que es fan en la comunitat de la física sobre si la física teòrica del sigle veintiuno s'està tornant massa matemàtica i està deixant arrere les seues raïls experimentals.

El camp emergent de les matemàtiques experimentals dilucida este debat de front, en enfocar-se en els experiments numèrics com la seua ferramenta principal per a l'exploració matemàtica.

Vore també

• Demostració en matemàtica
• Verificació de models
• Revisió de proves
• Càlcul simbòlic
• Raonament automàtic
• Verificació formal
• Seventeen or Bust
• Metamath