Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Information technology implications for mathematics a view from the French riviera

38 pages
Information technology implications for mathematics— a view from the French riviera Marco Maggesi and Carlos Simpson Laboratoire J. A. Dieudonne, CNRS UMR 6621 Universite de Nice-Sophia Antipolis . . . la traduction en langage formalise ne serait plus qu'un exercise de patience (sans doutes fort penible). —Nicolas Bourbaki Hanc marginis exiguitas non caperet. —Pierre de Fermat We feel that this context has now changed. For a long time, “mathemat- ics” and “computer science” have designated widely separated disciplines, overlapping only in areas which were considered “fringe” on either side. This was not really a historical view since Von Neumann, Turing and oth- ers were mathematicians who set off into the world of computers. We are now entering a time of reconvergence which has all kinds of implications. A prominent one is the increasing reality of computer proof verification as applied to standard mathematical work. This has been under development for quite a while, but just now it is becoming realistic to imagine applying it to a wide array of mathematical situations. The idea is to write mathematical documents in a language such that the mathematical accuracy is then verified by a computer program. This should be compared with other different but related utilisations of the computer: —typesetting: we are looking at having the computer understand the argu- ment, not just the visual expression on the page, nevertheless on a sociolog- ical level there are many similarities with the TEXproject; —computer algebra and other calculation systems: we are looking at the logical or “proof” aspect of mathematics,

  • effort can

  • higher-order than

  • can stimulate

  • order logic

  • proprietary system

  • his mathematical background

  • trivial theorem

  • apparently has latent

  • theorem-verification possibilities


Voir plus Voir moins
Informationtechnologyimplicationsformathematics—aviewfromtheFrenchrivieraMarcoMaggesiandCarlosSimpsonLaboratoireJ.A.Dieudonne´,CNRSUMR6621Universite´deNice-SophiaAntipolis...latraductionenlangageformalise´neseraitplusqu’unexercisedepatience(sansdoutesfortpe´nible).—NicolasBourbakiHancmarginisexiguitasnoncaperet.—PierredeFermatWefeelthatthiscontexthasnowchanged.Foralongtime,“mathemat-ics”and“computerscience”havedesignatedwidelyseparateddisciplines,overlappingonlyinareaswhichwereconsidered“fringe”oneitherside.ThiswasnotreallyahistoricalviewsinceVonNeumann,Turingandoth-ersweremathematicianswhosetoffintotheworldofcomputers.Wearenowenteringatimeofreconvergencewhichhasallkindsofimplications.Aprominentoneistheincreasingrealityofcomputerproofverificationasappliedtostandardmathematicalwork.Thishasbeenunderdevelopmentforquiteawhile,butjustnowitisbecomingrealistictoimagineapplyingittoawidearrayofmathematicalsituations.Theideaistowritemathematicaldocumentsinalanguagesuchthatthemathematicalaccuracyisthenverifiedbyacomputerprogram.Thisshouldbecomparedwithotherdifferentbutrelatedutilisationsofthecomputer:—typesetting:wearelookingathavingthecomputerunderstandtheargu-ment,notjustthevisualexpressiononthepage,neverthelessonasociolog-icalleveltherearemanysimilaritieswiththeTEXproject;—computeralgebraandothercalculationsystems:wearelookingatthelogicalor“proof”aspectofmathematics,includingalsotheproblemofintroducing,definingandmanipulatingnewabstractconcepts,whichisdif-ferentfromjusthavingthecomputerdoaspecificcalculation,butofcoursecalculationisoneprimordialaspectofmathematicalproofandoneofthebigproblemsishowtointegratethetwointoacoherentwhole;—computerproofsearch:wearenot,asabasicrequirement,askingthecomputertofindtheproofofsomething,onlytoverifytheproofthatthemathematiciangives.Oneofourfavoritereactionsfromacolleague(whoshallremainnameless)was:so,howisyourprojectoftrivializingmathematicsgoing?Butwearenottalkingabouttrivializingmathematics:themathematician1
hastosupplytheproof,becauseautomationcanperhapsdealwithwhatweregardassmalldetailsbutwillnever(?)replacethehumanworkofconcievingtheoutlineofacomplicatedargument.Afavoriteanalogyiswiththeconstructiontrade.Atfirst,everythingwasconstructedbylayingstoneorothermaterialbyhand.Ifyouwantedtobeintheconstructiontradeyouhadtoknowhowtolayastonewallthatwasstraight(noteasy).Nowdayswehavenewmaterialsandnewtools.Ifyouwanttobeintheconstructiontrade,youshouldknowhowtodriveatractorandhowtouseacircularsaw,butyoudon’treallyneedtoknowhowtobuildastonewallunlessyouspecializeinthatsortofthing.Whenwelookbackatthepyramidswesay“Wow!Ican’tbelievetheyactuallybuiltthosethingswithoutacrane!”.Inafewhundredyears,peoplewilllookbackatFermat’slasttheoremandsay“Wow!Ican’tbelievetheyactuallyprovedthatthingbyhand!”.Justastheadventofnewtechniquesintheconstructionindustryradi-callyalteredthelandscapeofbuildingswebuild,sotheadventofnewtoolsfordoingmathematicswillradicallyalterthetypeofmathematicswefind,andinwayswecanonlybarelyimaginerightnow.Itseemsimportantthatmathematiciansjointhefraysoastoopenupourunderstandingofwhatthefuturemighthold.Currentlymanydifferentsystemsareunderexperimentation:a“system”isaprogramwhichverifiesproofswritteninaspecifiedlanguage,plusallofthenecessarysupportmaterialincludingdocumentationforthelanguageandhowtoprovethingsinit;alibraryofresultsonwhichuserscanbuild;activesupportinthesenseofcontinuallyimprovingtheprogramtotakeintoaccountproblemswhichmaybeencounteredorimplementnewfunctional-ities,togetherwithmaintenanceofbackward-compatibilityforthelibrary(thisallrequiresanon-negligableamountofcomputerscience);andagroupofusersextendingbeyondtheimmediatecircleofthosewhoconcievedandmaintainedtheprogram.Thissubjecthasrecentlymadethenewsinseveraldifferentvenues,evenanarticleintheNewYorkTimes[Cha04].OneofthemorenotableeffortsatgettingthemathematicalcommunityinvolvedinthesubjectisThomasHales’“flyspeckproject”[Hal].Wewilllookatthecurrentstateoftheartwithrespecttoafewofthemainsystemswhicharecurrentlyavailable:ACL2,Coq,Isabelle,Mizar,NuPRL,...andalsobrieflyconsidersomeotherprojectswhicharenewerorpresentoriginalaspectssuchasPVS,Phox,MetaMath-Ghilbert,IMPS,...togetherwithsometransversalwebsitessuchasMKMnet,HELM,Omega,MathWeb/OMDoc.Wewillalsobrieflydiscusswhatthismightbringfor2
thefuture,includingweb-basedapproachestomathematicaleducation.Werestrictourattentionmostlytoopensystems.Thisispartlybecauseitismuchmoredifficulttoobtaininformationaboutproprietaryones(inparticularyouhavetopayforthem!),andalsothisinformationmaynotbeallthatrelevantotherthantousersoftheparticularsystem.Nonethe-lessweshouldmentiononemajorproprietarysystemMathematicawhichapparentlyhaslatenttheorem-verificationpossibilities.Mostoftheinformationherehasbeengainedbysearchingtheinternetwithstandardtools.Theinterestedreadermayreadilycontinuethatpathandfindmuchfulleranddeeperinformationthanwecouldcover.Thathav-ingbeensaid,wewillnotalwaysincludetheproperreferencesforsourcesbecause(1)therewouldbetoomany,and(2)itisallavailableontheweb(wetrytoavoidreferingtothingsyouwouldhavetopayfor).Alltold,thisrepresentsanotherinformation-technologyphenomenonwhichhasanenor-mousimpactonmathematics,whichwecoulddiscussatlengthbutthatwoulddepassthescopeofashortarticle.(Athirdphenomenon,thepos-sibilityofdoingmathematicalcommunicationbyvisioconference,doesn’tseemtoworkwellenoughyetthatwecoulddomorethanmentionitpar-enthetically.)1IwouldliketocertifymylatesttheoremWeexpectthattheformalizationofanontrivialtheoremmayrequireseveralyears.Togivetheidea,wecanciteThomasHaleswhoplanstocertifyhisproofoftheKeplerConjectureintwentyyears.Moreover,notallsubjectsofmathematicshaveanequalprobabilityofsuccessinformalizationwithtoday’stechnology:wemayexpectthatageometricalargumentof,say,knottheorywouldbeintrinsicallymoredifficulttoformalizethanaresultofalgebraorcombinatoriallogic.Asidefromthis,a“classical”mathematicianwouldprobablyneedtoenrichhismathematicalbackgroundwithavarietyoftopicsfromotherdomainssuchaslogicandcomputer-scienceinordertobeeffectiveintheproductionofaformaldocumentreadablebyacomputer.Thetrainingmayrequireanonnegligibletime(choosingasystem,understandingitslogicandbecomingproficientinitsuse,learningwhichresultsarealreadymadeavailableforthatsystem,etc).Ontheotherhand,thiseffortcanberepaidinseveralways.Firstofall,toreachacompleteformalizationofatheoremcanbeaveryinterestingexperience,bothforyoungandforseniorresearchers,thatcanberarely3
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin