Učitavanje video playera...
01:04:14
Ivica Kičić: Math Online Judge - web platforma za rješavanje matem. zadataka
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.
