Information technology implications for mathematics a view from the French riviera

Description

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

Sujets

• New York City
• Antipolis
• Simpson
• Neumann

Informations

• Publié par: pefav
• Nombre de lectures: 10
• Langue: English

Extrait

Informationtechnologyimplicationsformathematics— aviewfromtheFrenchriviera MarcoMaggesiandCarlosSimpson LaboratoireJ.A.Dieudonne´,CNRSUMR6621Universite´deNice-Sophia Antipolis ...latraductionenlangageformalise´neseraitplusqu’unexercisedepatience (sansdoutesfortpe´nible). —NicolasBourbaki Hancmarginisexiguitasnoncaperet. —PierredeFermat Wefeelthatthiscontexthasnowchanged.Foralongtime,“mathemat- ics”and“computerscience”havedesignatedwidelyseparateddisciplines, overlappingonlyinareaswhichwereconsidered“fringe”oneitherside. ThiswasnotreallyahistoricalviewsinceVonNeumann,Turingandoth- ersweremathematicianswhosetoffintotheworldofcomputers.Weare nowenteringatimeofreconvergencewhichhasallkindsofimplications. Aprominentoneistheincreasingrealityofcomputerproofverificationas appliedtostandardmathematicalwork.Thishasbeenunderdevelopment forquiteawhile,butjustnowitisbecomingrealistictoimagineapplying ittoawidearrayofmathematicalsituations. Theideaistowritemathematicaldocumentsinalanguagesuchthatthe mathematicalaccuracyisthenverifiedbyacomputerprogram.Thisshould becomparedwithotherdifferentbutrelatedutilisationsofthecomputer: —typesetting:wearelookingathavingthecomputerunderstandtheargu- ment,notjustthevisualexpressiononthepage,neverthelessonasociolog- icalleveltherearemanysimilaritieswiththeT E Xproject; —computeralgebraandothercalculationsystems:wearelookingatthe logicalor“proof”aspectofmathematics,includingalsotheproblemof introducing,definingandmanipulatingnewabstractconcepts,whichisdif- ferentfromjusthavingthecomputerdoaspecificcalculation,butofcourse calculationisoneprimordialaspectofmathematicalproofandoneofthe bigproblemsishowtointegratethetwointoacoherentwhole; —computerproofsearch:wearenot,asabasicrequirement,askingthe computertofindtheproofofsomething,onlytoverifytheproofthatthe mathematiciangives.Oneofourfavoritereactionsfromacolleague(who shallremainnameless)was: so,howisyourprojectoftrivializingmathematicsgoing? Butwearenottalkingabouttrivializingmathematics:themathematician 1

hastosupplytheproof,becauseautomationcanperhapsdealwithwhat weregardassmalldetailsbutwillnever(?)replacethehumanworkof concievingtheoutlineofacomplicatedargument. Afavoriteanalogyiswiththeconstructiontrade.Atfirst,everything wasconstructedbylayingstoneorothermaterialbyhand.Ifyouwantedto beintheconstructiontradeyouhadtoknowhowtolayastonewallthat wasstraight(noteasy).Nowdayswehavenewmaterialsandnewtools.If youwanttobeintheconstructiontrade,youshouldknowhowtodrivea tractorandhowtouseacircularsaw,butyoudon’treallyneedtoknowhow tobuildastonewallunlessyouspecializeinthatsortofthing.Whenwe lookbackatthepyramidswesay“Wow!Ican’tbelievetheyactuallybuilt thosethingswithoutacrane!”.Inafewhundredyears,peoplewilllook backatFermat’slasttheoremandsay“Wow!Ican’tbelievetheyactually provedthatthingbyhand!”. Justastheadventofnewtechniquesintheconstructionindustryradi- callyalteredthelandscapeofbuildingswebuild,sotheadventofnewtools fordoingmathematicswillradicallyalterthetypeofmathematicswefind, andinwayswecanonlybarelyimaginerightnow.Itseemsimportantthat mathematiciansjointhefraysoastoopenupourunderstandingofwhat thefuturemighthold. Currentlymanydifferentsystemsareunderexperimentation:a“system” isaprogramwhichverifiesproofswritteninaspecifiedlanguage,plusall ofthenecessarysupportmaterialincludingdocumentationforthelanguage andhowtoprovethingsinit;alibraryofresultsonwhichuserscanbuild; activesupportinthesenseofcontinuallyimprovingtheprogramtotakeinto accountproblemswhichmaybeencounteredorimplementnewfunctional- ities,togetherwithmaintenanceofbackward-compatibilityforthelibrary (thisallrequiresanon-negligableamountofcomputerscience);andagroup ofusersextendingbeyondtheimmediatecircleofthosewhoconcievedand maintainedtheprogram. Thissubjecthasrecentlymadethenewsinseveraldifferentvenues,even anarticleintheNewYorkTimes[Cha04].Oneofthemorenotableefforts atgettingthemathematicalcommunityinvolvedinthesubjectisThomas Hales’“flyspeckproject”[Hal]. Wewilllookatthecurrentstateoftheartwithrespecttoafewofthe mainsystemswhicharecurrentlyavailable:ACL2,Coq,Isabelle,Mizar, NuPRL,...andalsobrieflyconsidersomeotherprojectswhicharenewer orpresentoriginalaspectssuchasPVS,Phox,MetaMath-Ghilbert,IMPS, ...togetherwithsometransversalwebsitessuchasMKMnet,HELM,Omega, MathWeb/OMDoc.Wewillalsobrieflydiscusswhatthismightbringfor 2

thefuture,includingweb-basedapproachestomathematicaleducation. Werestrictourattentionmostlytoopensystems.Thisispartlybecause itismuchmoredifficulttoobtaininformationaboutproprietaryones(in particularyouhavetopayforthem!),andalsothisinformationmaynot beallthatrelevantotherthantousersoftheparticularsystem.Nonethe- lessweshouldmentiononemajorproprietarysystemMathematicawhich apparentlyhaslatenttheorem-verificationpossibilities. Mostoftheinformationherehasbeengainedbysearchingtheinternet withstandardtools.Theinterestedreadermayreadilycontinuethatpath andfindmuchfulleranddeeperinformationthanwecouldcover.Thathav- ingbeensaid,wewillnotalwaysincludetheproperreferencesforsources because(1)therewouldbetoomany,and(2)itisallavailableontheweb (wetrytoavoidreferingtothingsyouwouldhavetopayfor).Alltold,this representsanotherinformation-technologyphenomenonwhichhasanenor- mousimpactonmathematics,whichwecoulddiscussatlengthbutthat woulddepassthescopeofashortarticle.(Athirdphenomenon,thepos- sibilityofdoingmathematicalcommunicationbyvisioconference,doesn’t seemtoworkwellenoughyetthatwecoulddomorethanmentionitpar- enthetically.) 1“Iwouldliketocertifymylatesttheorem” Weexpectthattheformalizationofanontrivialtheoremmayrequireseveral years.Togivetheidea,wecanciteThomasHaleswhoplanstocertifyhis proofoftheKeplerConjectureintwentyyears. Moreover,notallsubjectsofmathematicshaveanequalprobability ofsuccessinformalizationwithtoday’stechnology:wemayexpectthat ageometricalargumentof,say,knottheorywouldbeintrinsicallymore difficulttoformalizethanaresultofalgebraorcombinatoriallogic. Asidefromthis,a“classical”mathematicianwouldprobablyneedto enrichhismathematicalbackgroundwithavarietyoftopicsfromother domainssuchaslogicandcomputer-scienceinordertobeeffectiveinthe productionofaformaldocumentreadablebyacomputer.Thetraining mayrequireanonnegligibletime(choosingasystem,understandingits logicandbecomingproficientinitsuse,learningwhichresultsarealready madeavailableforthatsystem,etc). Ontheotherhand,thiseffortcanberepaidinseveralways.Firstof all,toreachacompleteformalizationofatheoremcanbeaveryinteresting experience,bothforyoungandforseniorresearchers,thatcanberarely 3