Šveicarijoje įsikūrusi „Justin Sun“ biuras spalio 5 dieną pranešė apie pirmuosius patvirtintus „Justin Sun Prize“ laureatus. Apdovanojimas atiteko nepriklausomam tyrėjui Wouteriui van Doornui, matematikos doktorantui Quanyu Tang ir Nandzingo Pietryčių universiteto tyrėjai Yanyang Li už darbus, susijusius su šešiais vadinamaisiais Erdőso uždaviniais.
Erdőso uždaviniai – tai vengrų matematiko Paulo Erdőso suformuluoti arba išpopuliarinti klausimai skaičių teorijoje ir kombinatorikoje. Jie dažnai skamba paprastai, tačiau jų sprendimui prireikia metų ar net dešimtmečių, o dalis problemų iki šiol lieka atviros.
Kas įvertinta ir kodėl svarbu
Pasak apdovanojimo organizatorių, van Doornas, Tang ir Li bendradarbiavo spręsdami Erdőso problemą Nr. 650, kurioje siekta tiksliai nustatyti, kiek sveikųjų skaičių visuomet galima suporuoti su skirtingais jų kartotiniais apibrėžtame intervale. Tai tipinis Erdőso stiliaus klausimas: formuluotė trumpa, tačiau už jos slypi sudėtinga struktūra apie skaičių išsidėstymą ir dėsningumus.
Kartu pabrėžiama, kad apdovanojime vertinamas ne tik naujas matematinis rezultatas, bet ir įrodymo patikrinamumas. Dėl to dalis darbų buvo parengti taip, kad juos būtų galima formaliai verifikuoti naudojant „Lean“ – programinę aplinką, leidžiančią kompiuteriu tikrinti matematinių įrodymų logiką.
DI vaidmuo sprendimuose
Vienas ryškiausių šio pranešimo akcentų – žmonių ir DI bendradarbiavimo elementas. Nurodoma, kad rengiant problemos Nr. 650 sprendimą DI įrankiai prisidėjo kuriant įrodymo strategiją, o formalizavimo etape padėjo rasti ir užtaisyti spragą, kad įrodymas atitiktų griežtus kompiuterinės verifikacijos reikalavimus.
„Ši patirtis parodė, kaip viešas grįžtamasis ryšys gali patikslinti tyrimo klausimą, o DI padedamas atradimas gali sujungti matematinį sprendimą, bendradarbiavimą ir griežtą verifikaciją“, – sakė Quanyu Tang.
Pranešime taip pat teigiama, kad van Doornas parengė kompiuteriu patikrinamus „Lean“ įrodymus kelioms kitoms Erdőso katalogo problemoms, susijusioms su pirminių daugiklių apribojimais ir skaičių aibių savybėmis. Tuo metu Tang atskirai išsprendė problemą Nr. 1 044, kurioje buvo nustatyta tiksli apatinė riba tam tikrų polinomais apibrėžtų sričių ribų ilgiams, o kartu su Li prisidėjo prie problemos Nr. 1 196 sprendimo komandoje.
Ką tai reiškia matematikai
Pastaraisiais metais matematikoje ryškėja dvi lygiagrečios kryptys: DI įrankių naudojimas idėjoms generuoti ir formaliųjų įrodymų tikrinimo plėtra, siekiant išvengti klaidų sudėtinguose argumentuose. Šiame kontekste „Justin Sun Prize“ pristatomas kaip iniciatyva, bandanti sujungti abi kryptis, skatindama tiek sprendimų paiešką, tiek jų patikimumą.
Organizatoriai pabrėžia, kad apdovanojimas orientuotas į įrodymo stiprumą ir patikrinamumą, o ne į autorių statusą ar institucijų prestižą. Tai ypač aktualu šiandien, kai augant tyrimų apimtims ir sudėtingumui vis didesnę reikšmę įgauna skaidrumas, atkartojamumas ir aiškiai patikrinamos metodikos.