Datastøttet bevis - Computer-assisted proof

Et datamaskinassistert bevis er et matematisk bevis som i det minste delvis er generert av datamaskinen .

De fleste dataassisterte bevis hittil har vært implementeringer av store bevis-for-utmattelse av en matematisk teorem . Tanken er å bruke et dataprogram til å utføre lange beregninger, og å gi et bevis på at resultatet av disse beregningene innebærer gitt setning. I 1976 var firefargesetningen det første store teoremet som ble verifisert ved hjelp av et dataprogram .

Det har også blitt gjort forsøk innen kunstig intelligensforskning for å lage mindre, eksplisitte, nye bevis på matematiske teoremer fra bunnen og opp ved hjelp av maskinelle resonnementsteknikker som heuristisk søk. Slike automatiserte teoremprovers har bevist en rekke nye resultater og funnet nye bevis for kjente setninger. I tillegg lar interaktive bevisassistenter matematikere utvikle lesbare bevis som likevel er formelt verifisert for korrekthet. Siden disse bevisene generelt kan undersøkes av mennesker (om enn med vanskeligheter, som med beviset på Robbins-formodningen ), deler de ikke de kontroversielle implikasjonene av dataassisterte bevis for utmattelse.

Metoder

En metode for bruk av datamaskiner i matematiske bevis er ved hjelp av såkalt validert numerikk eller streng numerikk. Dette betyr å beregne numerisk, men med matematisk strenghet. Man bruker sett-verdifull aritmetikk og inkluderingsprinsipp for å sikre at den verdivurderte utgangen til et numerisk program omslutter løsningen av det opprinnelige matematiske problemet. Dette gjøres ved å kontrollere, omslutte og spre avrundings- og avkortingsfeil ved å bruke for eksempel intervallregning . Mer presist, man reduserer beregningen til en sekvens av elementære operasjoner, sier . I en datamaskin avrundes resultatet av hver elementære operasjon av datamaskinens presisjon. Imidlertid kan man konstruere et intervall gitt av øvre og nedre grenser på resultatet av en elementær operasjon. Deretter fortsetter man med å erstatte tall med intervaller og utføre elementære operasjoner mellom slike intervaller med representerbare tall.

Filosofiske innvendinger

Hovedartikkel: Ikke-undersøkelig bevis

Datastøttede bevis er gjenstand for noen kontroverser i den matematiske verden, med Thomas Tymoczko som først formulerte innvendinger. De som holder seg til Tymoczkos argumenter mener at lange datamaskinassisterte bevis ikke på en eller annen måte er 'ekte' matematiske bevis fordi de involverer så mange logiske trinn at de ikke praktisk talt kan verifiseres av mennesker, og at matematikere faktisk blir bedt om å erstatte logisk fradrag fra antatte aksiomer med tillit til en empirisk beregningsprosess, som potensielt påvirkes av feil i dataprogrammet, samt defekter i kjøretidsmiljøet og maskinvaren.

Andre matematikere mener at lange datamaskinassisterte bevis må betraktes som beregninger , snarere enn bevis : selve bevisalgoritmen bør bevises gyldig, slik at bruken da kan betraktes som en ren "verifikasjon". Argumenter om at datamaskinassisterte bevis er utsatt for feil i kildeprogrammene, kompilatorene og maskinvaren, kan løses ved å gi et formelt bevis på korrekthet for dataprogrammet (en tilnærming som ble brukt på firefargesetningen i 2005) som samt replikere resultatet ved hjelp av forskjellige programmeringsspråk, forskjellige kompilatorer og annen maskinvare.

En annen mulig måte å verifisere dataassisterte bevis på er å generere sine resonnementstrinn i en maskinlesbar form, og deretter bruke et korrekturprogram for å demonstrere at de er korrekte. Siden validering av et gitt bevis er mye enklere enn å finne et bevis, er kontrollprogrammet enklere enn det originale assistentprogrammet, og det er tilsvarende lettere å få tillit til at det er riktig. Imidlertid appellerer ikke denne tilnærmingen til å bruke et dataprogram for å bevise at utgangen til et annet program er korrekt, til datasikker skeptikere, som ser på det som å legge til et nytt lag av kompleksitet uten å ta opp det opplevde behovet for menneskelig forståelse.

Et annet argument mot dataassisterte bevis er at de mangler matematisk eleganse- at de ikke gir innsikt eller nye og nyttige konsepter. Faktisk er dette et argument som kan fremmes mot ethvert langt bevis ved utmattelse.

Et annet filosofisk spørsmål som tas opp av dataassisterte bevis er om de gjør matematikk til en kvasi-empirisk vitenskap , der den vitenskapelige metoden blir viktigere enn anvendelsen av ren fornuft innen abstrakte matematiske begreper. Dette relaterer direkte til argumentet innen matematikk om matematikk er basert på ideer, eller "bare" en øvelse i formell symbolmanipulering. Det reiser også spørsmålet om alle mulige matematiske objekter i en eller annen forstand "allerede eksisterer" ifølge platonistisk syn, om datamaskinassistert matematikk er en observasjonsvitenskap som astronomi, snarere enn en eksperimentell som fysikk eller kjemi. Denne kontroversen innen matematikk forekommer samtidig som det blir stilt spørsmål i fysikkmiljøet om hvorvidt teoretisk fysikk fra det tjueførste århundre blir for matematisk og etterlater sine eksperimentelle røtter.

Det nye feltet for eksperimentell matematikk konfronterer denne debatten direkte ved å fokusere på numeriske eksperimenter som hovedverktøy for matematisk leting.

applikasjoner

Teoremer viste seg ved hjelp av dataprogrammer

Inkludering i denne listen betyr ikke at det finnes et formelt datamaskinsjekket bevis, men at et dataprogram har vært involvert på en eller annen måte. Se hovedartiklene for detaljer.

Teoremer til salgs

I 2010 tilbød akademikere ved University of Edinburgh folk sjansen til å "kjøpe sin egen teorem" opprettet gjennom et datamaskinassistert bevis. Denne nye teoremet ville bli oppkalt etter kjøperen.

Se også

Referanser

Videre lesning

Eksterne linker