\u0160veicarijoje \u012fsik\u016brusi \u201eJustin Sun\u201c biuras spalio 5 dien\u0105 prane\u0161\u0117 apie pirmuosius patvirtintus \u201eJustin Sun Prize\u201c laureatus. Apdovanojimas atiteko nepriklausomam tyr\u0117jui Wouteriui van Doornui, matematikos doktorantui Quanyu Tang ir Nandzingo Pietry\u010di\u0173 universiteto tyr\u0117jai Yanyang Li u\u017e darbus, susijusius su \u0161e\u0161iais vadinamaisiais Erd\u0151so u\u017edaviniais.<\/p>\n
Erd\u0151so u\u017edaviniai \u2013 tai vengr\u0173 matematiko Paulo Erd\u0151so suformuluoti arba i\u0161populiarinti klausimai skai\u010di\u0173 teorijoje ir kombinatorikoje. Jie da\u017enai skamba paprastai, ta\u010diau j\u0173 sprendimui prireikia met\u0173 ar net de\u0161imtme\u010di\u0173, o dalis problem\u0173 iki \u0161iol lieka atviros.<\/p>\n
Pasak apdovanojimo organizatori\u0173, van Doornas, Tang ir Li bendradarbiavo spr\u0119sdami Erd\u0151so problem\u0105 Nr. 650, kurioje siekta tiksliai nustatyti, kiek sveik\u0173j\u0173 skai\u010di\u0173 visuomet galima suporuoti su skirtingais j\u0173 kartotiniais apibr\u0117\u017etame intervale. Tai tipinis Erd\u0151so stiliaus klausimas: formuluot\u0117 trumpa, ta\u010diau u\u017e jos slypi sud\u0117tinga strukt\u016bra apie skai\u010di\u0173 i\u0161sid\u0117stym\u0105 ir d\u0117sningumus.<\/p>\n
Kartu pabr\u0117\u017eiama, kad apdovanojime vertinamas ne tik naujas matematinis rezultatas, bet ir \u012frodymo patikrinamumas. D\u0117l to dalis darb\u0173 buvo parengti taip, kad juos b\u016bt\u0173 galima formaliai verifikuoti naudojant \u201eLean\u201c \u2013 programin\u0119 aplink\u0105, leid\u017eian\u010di\u0105 kompiuteriu tikrinti matematini\u0173 \u012frodym\u0173 logik\u0105.<\/p>\n
Vienas ry\u0161kiausi\u0173 \u0161io prane\u0161imo akcent\u0173 \u2013 \u017emoni\u0173 ir DI bendradarbiavimo elementas. Nurodoma, kad rengiant problemos Nr. 650 sprendim\u0105 DI \u012frankiai prisid\u0117jo kuriant \u012frodymo strategij\u0105, o formalizavimo etape pad\u0117jo rasti ir u\u017etaisyti sprag\u0105, kad \u012frodymas atitikt\u0173 grie\u017etus kompiuterin\u0117s verifikacijos reikalavimus.<\/p>\n
\u201e\u0160i patirtis parod\u0117, kaip vie\u0161as gr\u012f\u017etamasis ry\u0161ys gali patikslinti tyrimo klausim\u0105, o DI padedamas atradimas gali sujungti matematin\u012f sprendim\u0105, bendradarbiavim\u0105 ir grie\u017et\u0105 verifikacij\u0105\u201c, \u2013 sak\u0117 Quanyu Tang.<\/p>\n
Prane\u0161ime taip pat teigiama, kad van Doornas pareng\u0117 kompiuteriu patikrinamus \u201eLean\u201c \u012frodymus kelioms kitoms Erd\u0151so katalogo problemoms, susijusioms su pirmini\u0173 daugikli\u0173 apribojimais ir skai\u010di\u0173 aibi\u0173 savyb\u0117mis. Tuo metu Tang atskirai i\u0161sprend\u0117 problem\u0105 Nr. 1 044, kurioje buvo nustatyta tiksli apatin\u0117 riba tam tikr\u0173 polinomais apibr\u0117\u017et\u0173 sri\u010di\u0173 rib\u0173 ilgiams, o kartu su Li prisid\u0117jo prie problemos Nr. 1 196 sprendimo komandoje.<\/p>\n
Pastaraisiais metais matematikoje ry\u0161k\u0117ja dvi lygiagre\u010dios kryptys: DI \u012franki\u0173 naudojimas id\u0117joms generuoti ir formali\u0173j\u0173 \u012frodym\u0173 tikrinimo pl\u0117tra, siekiant i\u0161vengti klaid\u0173 sud\u0117tinguose argumentuose. \u0160iame kontekste \u201eJustin Sun Prize\u201c pristatomas kaip iniciatyva, bandanti sujungti abi kryptis, skatindama tiek sprendim\u0173 paie\u0161k\u0105, tiek j\u0173 patikimum\u0105.<\/p>\n
Organizatoriai pabr\u0117\u017eia, kad apdovanojimas orientuotas \u012f \u012frodymo stiprum\u0105 ir patikrinamum\u0105, o ne \u012f autori\u0173 status\u0105 ar institucij\u0173 presti\u017e\u0105. Tai ypa\u010d aktualu \u0161iandien, kai augant tyrim\u0173 apimtims ir sud\u0117tingumui vis didesn\u0119 reik\u0161m\u0119 \u012fgauna skaidrumas, atkartojamumas ir ai\u0161kiai patikrinamos metodikos.<\/p>\n","protected":false},"excerpt":{"rendered":"
\u201eJustin Sun Prize\u201c paskelb\u0117 pirmuosius laureatus: \u012fvertinti sprendimai Erd\u0151so u\u017edaviniams, kuriuose derinti DI \u012frankiai ir formalus \u012frodym\u0173 tikrinimas.<\/p>\n","protected":false},"author":0,"featured_media":61845,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[94],"tags":[115,47118,47120,40570,114,47121,47119],"miestas":[],"class_list":["post-61844","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-finansai","tag-bitcoin","tag-erdoso-uzdaviniai","tag-formalus-irodymu-tikrinimas","tag-kombinatorika","tag-kriptovaliutos","tag-lean","tag-skaiciu-teorija"],"acf":[],"_links":{"self":[{"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/posts\/61844","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/types\/post"}],"replies":[{"embeddable":true,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/comments?post=61844"}],"version-history":[{"count":0,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/posts\/61844\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/media\/61845"}],"wp:attachment":[{"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/media?parent=61844"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/categories?post=61844"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/tags?post=61844"},{"taxonomy":"miestas","embeddable":true,"href":"https:\/\/cp.snarskis.lt\/index.php\/wp-json\/wp\/v2\/miestas?post=61844"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}