Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/599| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | Marić, Filip | en_US |
| dc.contributor.author | Stojanović-Ðurdević, Sana | en_US |
| dc.date.accessioned | 2022-08-13T15:50:05Z | - |
| dc.date.available | 2022-08-13T15:50:05Z | - |
| dc.date.issued | 2020-10-30 | - |
| dc.identifier.issn | 20752180 | en |
| dc.identifier.uri | https://research.matf.bg.ac.rs/handle/123456789/599 | - |
| dc.description.abstract | The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course”Introduction to Interactive Theorem Proving”. | en |
| dc.relation.ispartof | Electronic Proceedings in Theoretical Computer Science, EPTCS | en_US |
| dc.title | Formalizing IMO problems and solutions in Isabelle/HOL | en_US |
| dc.type | Conference Paper | en_US |
| dc.identifier.doi | 10.4204/EPTCS.328.3 | - |
| dc.identifier.scopus | 2-s2.0-85101257188 | - |
| dc.identifier.url | https://api.elsevier.com/content/abstract/scopus_id/85101257188 | - |
| dc.contributor.affiliation | Informatics and Computer Science | en_US |
| dc.relation.firstpage | 35 | en_US |
| dc.relation.lastpage | 55 | en_US |
| dc.relation.volume | 328 | en_US |
| item.fulltext | No Fulltext | - |
| item.openairecristype | http://purl.org/coar/resource_type/c_18cf | - |
| item.cerifentitytype | Publications | - |
| item.grantfulltext | none | - |
| item.openairetype | Conference Paper | - |
| crisitem.author.dept | Informatics and Computer Science | - |
| crisitem.author.orcid | 0000-0001-7219-6960 | - |
| Appears in Collections: | Research outputs | |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.