Seminar za matematičku logiku i računarstvo i Seminar za edukacijsku matematiku

Na zajedničkom sastanku Seminara za matematičku logiku i računarstvo te Seminara za edukacijsku matematiku, u ponedjeljak 24. studenoga 2025. u 17:15 sati, u predavaonici 105, PMF-MO, Ivica Kičić će održati predavanje

Math Online Judge: web platforma za rješavanje matematičkih zadataka u formalnim jezicima

Sažetak: U posljednjih desetak godina formalna verifikacija, potpomognuta sustavima poput Lean-a i Rocq-a, sve se češće koristi u matematičkom istraživanju — od provjere dokaza do automatiziranog dokazivanja teorema. Iako ti sustavi imaju znatan potencijal, njihovo je usvajanje otežano tehničkom složenošću i nedostatkom pristupačnih okruženja koja bi olakšala prve korake u radu s takvim alatima.

Usporedno s time, u informatičkom obrazovanju široko su prihvaćene tzv. „Online Judge“ platforme — web sustavi koji nude opsežne zbirke zadataka i omogućuju automatsku provjeru ispravnosti rješenja. Njihov natjecateljski karakter i neposredna povratna informacija pokazali su se vrlo učinkovitim u poticanju učenja programiranja.

Ovaj seminar predstavlja ideju i rani prototip takve platforme, prilagođene rješavanju matematičkih zadataka u formalnim jezicima. Sustav bi omogućio automatsku evaluaciju rješenja te strukturirano napredovanje kroz razine složenosti, stvarajući time okruženje koje potiče učenje i eksperimentiranje s formalnim metodama.

Cilj seminara je otvoriti raspravu o tome u kojoj bi mjeri ovakav sustav mogao doprinijeti edukaciji o formalnim jezicima te koliko bi mogao pomoći u popularizaciji formalne verifikacije i njenog uvođenja u širu matematičku praksu.