Kevin Buzzard: Kako začeti revolucijo v matematiki?

Gost današnjega intervjuja znanstvene redakcije je profesor matematike Kevin Buzzard z londonskega Imperial Collegea. V svojem raziskovalnem delu se ukvarja z vprašanji o naravnih številih, ki so pogosto relativno enostavno opisljiva in neverjetno težko razrešljiva. Slaven primer je Fermatov zadnji nedokazan teorem, ki je potrditev o neresničnosti dobil šele 350 let po oblikovanju. Sogovorec se od leta 2017 ukvarja s formaliziranjem matematičnih dokazov -  od vsebin, ki jih srečamo na dodiplomskem študiju, do algebraične teorije števil. To pomeni prevajanje izjav področja v jezik, razumljiv računalnikom. Formalni jezik je nabor simbolov, ki izražajo objekte in razmerja med njimi, v tem konkretnem primeru si jih lahko zamislimo kot celoten znakovni standard UNICODE. Sodobni interaktivni računalniški programi lahko ta zapis interpretirajo kot matematični stavek ali teorem in odločijo o njegovi veljavnosti.

Prakticiranje matematike v takem sožitju z računalnikom sicer ni novo, vendar trenutno ni zelo razširjena praksa. Najprej smo profesorja Buzzarda v pogovoru vprašali, kakšen je trenuten ugled te discipline in katere zgodovinske izkušnje oblikujejo mnenja matematikov o njej.

Izjava.

Danes smo priča nenadzorovanemu hajpu o sposobnosti računalniških programov, da opravljajo naloge, ki so bile dolgo mišljene kot izključna pritiklina ljudi. Umetna inteligenca nevronskih mrež tako že davno prekaša ljudi v šahu, nedavno pa je presegla tudi visoko sofisticirane klasične programe. Podobno se je zgodilo tudi v igri go. Kaj bi torej lahko ustavilo programe, da v kratkem popolnoma prevzamejo vse funkcije človeške inteligence in začnejo odkrivati tudi novo matematiko?

Izjava.

S spremembami v sestavi skupnosti, ki prispeva k formaliziranju matematike, se je v zadnjem letu spremenil tudi domet za matematiko, ki jo lahko skupnost naslavlja v formaliziranem sistemu. V zadnjem letu smo tako priča prodoru pristopa v visoke kroge najnaprednejših področij sodobne matematike – v smislu prestiža, ki jim ga pripisujejo staroste področja. Sogovorca smo vprašali O aktualnem dogajanju.

Izjava.

Na kakšen odziv pa je ta zgodba naletela pri stroki?

Izjava.

Sogovorec se je s formalizirano matematiko začel ukvarjati pravzaprav po naključju, kot del svojega pedagoškega dela. Druga plat trendovske matematike je bila zanj tako ustanovitev študentskega kluba Xena Project in z njim povezanega bloga, ki ju lahko oba najdemo na medmrežju. Vprašali smo ga o njegovi motivaciji in pristopu pri uvajanju novega kontinenta v izobraževanje ter o lekcijah, ki jih je ob tem pridobil.

Izjava.