LLM chatbot kao pomoćnik za dokazivanje matematičkih teorema

Rad donosi praktičan prikaz primjene umjetne inteligencije u matematici, s naglaskom na to koliko LLM modeli mogu pomoći pri dokazivanju složenih tvrdnji i teorema.

SAŽETAK

Autori prikazuju kako su im LLM chatbotovi (ChatGPT, Gemini, Claude, DeepSeek) pomagali u dokazivanju jedne matematičke tvrdnje vezane za najkraći put između dvije točke položene na suprotnim bazama pravilnog n-terokuta. Preciznije, ta tvrdnja je ova: „Svaka neparna pravilna prizma ima barem jedan p-neovisan kraći put, tj. kraći put čija duljina ne ovisi o udaljenosti točaka A i B („mrava“ i „meda“) od ruba, dok ga parne prizme nemaju. Duljina najkraćeg puta je: d = b √(k² + 2 cos(π/n) k + 1)”.

Početna verzija tog matematičkog problema (i računalne igre) prikazana je na CASE 2020 konferenciji, pod nazivom „Mrav i med na prizmi (i valjku) – matematička podloga i koncept igre“.

U novom radu naglasak je na tome koliko kod dokazivanja matematičkih teorema može koristiti „čisti“ LLM chatbot, bez specijaliziranih dokazivača teorema (theorem provera).