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.