Ostatnie lata obfitują w zdumiewające w swojej śmiałości i skali doniesienia o tym czy i jak AI, w szczególności metody oparte na wielkich modelach języka, mają zrewolucjonizować naukę, w tym informatykę i matematykę. Prelegent przyjrzał się z bliska tym doniesieniom, z perspektywy zarówno praktykującego matematyka, jak i zaangażowanego beta-testera takich systemów. W wykładzie prelegent przedstawi kilka spektakularnych przykładów, gdzie oparte na transformerach sieci neuronowe potrafią wyprodukować sensownie wyglądający dowód matematyczny, a zarazem potrafią mylić się w co drugim zdaniu. W opowieść będą włączone też metody formalizacji dowodów oparte na programowaniu funkcyjnym i zobaczymy, czy na horyzoncie nie pojawia się jednak wizja matematyki zmechanizowanej, w której człowiekowi pozostaje być (tylko) wiecznym źródłem inspiracji.

Wykład odbędzie się we wtorek 9 grudnia na Wydziale Matematyki i Informatyki UWM przy ul. Słonecznej 54 w auli C2 w godz. od 11:30 do 12:30.