Ndërtimi i Bibliotekës Matematikore të së Ardhmes

Çdo ditë, dhjetëra matematikanë me të njëjtin mendim mblidhen në një forum në internet të quajtur Zulip për të ndërtuar atë që ata besojnë se është e ardhmja e fushës së tyre.

Ata janë të gjithë adhurues të një programi softuerësh të quajtur Lean. Është një “asistent provë” që, në parim, mund t’i ndihmojë matematikanët të shkruajnë prova. Por përpara se Lean ta bëjë këtë, vetë matematikanët duhet të fusin manualisht matematikën në program, duke përkthyer mijëra vjet njohuri të akumuluara në një formë që Lean mund ta kuptojë.

Për shumë nga njerëzit e përfshirë, virtytet e përpjekjes janë pothuajse të vetëkuptueshme.

“Është thelbësisht e qartë se kur dixhitalizon diçka, mund ta përdorësh në mënyra të reja”, tha Kevin Buzzard nga Imperial College London. “Ne do të dixhitalizojmë matematikën dhe kjo do ta bëjë atë më të mirë.”

Dixhitalizimi i matematikës është një ëndërr e vjetër. Përfitimet e pritshme variojnë nga gjërat e zakonshme – kompjuterët që vlerësojnë detyrat e shtëpisë së studentëve – deri tek ato transhendente: përdorimi i inteligjencës artificiale për të zbuluar matematikë të re dhe për të gjetur zgjidhje të reja për problemet e vjetra. Matematikanët presin që asistentët e provave të mund të shqyrtojnë gjithashtu parashtresat e ditarit, duke gjetur gabime që recensentët njerëzorë i humbasin herë pas here dhe të trajtojnë punën e lodhshme teknike që shkon në plotësimin e të gjitha detajeve të një prove.

Por së pari, matematikanët që mblidhen në Zulip duhet t’i japin Lean-it atë që përbën një bibliotekë të njohurive universitare të matematikës, dhe ata janë vetëm në gjysmë të rrugës. Lean nuk do të zgjidhë problemet e hapura së shpejti, por njerëzit që punojnë në të janë pothuajse të sigurt se në pak vite programi të paktën do të jetë në gjendje të kuptojë pyetjet në një provim përfundimtar të vitit të lartë.

Dhe pas kësaj, kush e di? Matematikanët që marrin pjesë në këto përpjekje nuk e parashikojnë plotësisht se për çfarë do të jetë e mirë matematika dixhitale.

“Ne nuk e dimë vërtet se ku po shkojmë,” tha Sébastien Gouëzel nga Universiteti i Rennes.

Gjatë verës, një grup përdoruesish Lean me përvojë drejtuan një seminar në internet të quajtur “Lean for the Curious Mathematician”. Në sesionin e parë, Scott Morrison nga Universiteti i Sidneit demonstroi se si të shkruani një provë në program.

Ai filloi duke shtypur deklaratën që donte të provonte në sintaksë se Lean kupton. Në anglisht të thjeshtë, përkthehet në “Ka pafundësisht shumë numra të thjeshtë”. Ka disa mënyra për të vërtetuar këtë deklaratë, por Morrison donte të përdorte një modifikim të lehtë të të parës së zbuluar ndonjëherë, provën e Euklidit nga viti 300 pes, e cila përfshin shumëzimin e të gjitha numrave të parë të njohur së bashku dhe shtimin e 1 për të gjetur një kryeministër të ri (ose vetë produkti ose një nga pjesëtuesit e tij do të jetë i thjeshtë). Zgjedhja e Morrison pasqyroi diçka themelore në lidhje me përdorimin e Lean: Përdoruesi duhet të krijojë vetë idenë e madhe të provës.

“Ju jeni përgjegjës për sugjerimin e parë,” tha Morrison në një intervistë të mëvonshme.

Pasi shtypi deklaratën dhe zgjodhi një strategji, Morrison kaloi disa minuta duke paraqitur strukturën e provës: Ai përcaktoi një sërë hapash të ndërmjetëm, secili prej të cilëve ishte relativisht i thjeshtë për t’u provuar më vete. Ndërsa Lean nuk mund të dalë me strategjinë e përgjithshme të një prove, shpesh mund të ndihmojë në ekzekutimin e hapave më të vegjël dhe konkretë. Duke e ndarë provën në nën-detyra të menaxhueshme, Morrison ishte paksa si një kuzhinier që udhëzon kuzhinierët e linjës të presin një qepë dhe të ziejnë një zierje. “Është në këtë pikë që ju shpresoni që Lean të marrë përsipër dhe të fillojë të jetë i dobishëm,” tha Morrison.

Lean i kryen këto detyra të ndërmjetme duke përdorur procese të automatizuara të quajtura “taktika”. Mendoni për to si algoritme të shkurtra të përshtatura për të kryer një punë shumë specifike.

Ndërsa punonte me provat e tij, Morrison drejtoi një taktikë të quajtur “kërkim bibliotekar”. Ai zbuloi bazën e të dhënave të Lean-it të rezultateve matematikore dhe ktheu disa teorema që mendonte se mund të plotësonin detajet e një seksioni të veçantë të provës. Taktika të tjera kryejnë punë të ndryshme matematikore. Njëri, i quajtur “linarith”, mund të marrë një grup pabarazish midis, të themi, dy numrave realë dhe të konfirmojë për ju se një pabarazi e re që përfshin një numër të tretë është e vërtetë: Nëse a është 2 dhe b është më e madhe se a, atëherë 3a + 4b është më i madh se 12. Një tjetër bën pjesën më të madhe të punës për zbatimin e rregullave bazë algjebrike si asociativiteti.

“Dy vjet më parë do t’ju duhej të [aplikoni pronësinë shoqëruese] vetë në Lean,” tha Amelia Livingston, një diplomë universitare e matematikës në Imperial College London, e cila po mëson Lean nga Buzzard. “Pastaj [dikush] shkroi një taktikë që mund t’i bëjë të gjitha për ju. Sa herë që e përdor, jam shumë i lumtur.”

Gjithsej, Morrisonit iu deshën 20 minuta për të përfunduar provën e Euklidit. Në disa vende i plotësonte vetë detajet; në të tjera ai përdorte taktika për ta bërë atë për të. Në çdo hap, Lean kontrollonte për t’u siguruar që puna e tij ishte në përputhje me rregullat logjike themelore të programit, të cilat janë shkruar në një gjuhë zyrtare të quajtur teoria e tipit të varur.

“Është si një aplikacion sudoku. Nëse bëni një lëvizje që nuk është e vlefshme, ajo do të jetë e zhurmshme, “tha Buzzard. Në fund, Lean vërtetoi se provat e Morrison funksionuan.

Ushtrimi ishte emocionues në mënyrën se si është gjithmonë kur teknologjia ndërhyn për të bërë diçka që e bënit vetë. Por prova e Euklidit ka ekzistuar për më shumë se 2000 vjet. Llojet e problemeve për të cilat matematicienët kujdesen sot janë aq të ndërlikuara sa Lean nuk mund t’i kuptojë ende pyetjet, e lëre më të mbështesë procesin e përgjigjes së tyre.

“Ka të ngjarë të kalojnë dekada përpara se ky të jetë një mjet kërkimi,” tha Heather Macbeth nga Universiteti Fordham, një përdorues tjetër i Lean.

Pra, përpara se matematikanët të mund të punojnë me Lean për problemet që ata vërtet i interesojnë, ata duhet ta pajisin programin me më shumë matematikë. Kjo është në fakt një detyrë relativisht e drejtpërdrejtë.