The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems. - Libor Barto; Michael Kompatscher; Miroslav Olsák; Trung Van Pham; Michael Pinsker (LICS, 2017)

Reinforcement Learning of Theorem Proving. - Cezary Kaliszyk; Josef Urban; Henryk Michalewski; Miroslav Olsák (NeurIPS, 2018)

Dichotomy for Symmetric Boolean PCSPs. - Miron Ficak; Marcin Kozik; Miroslav Olsák; Szymon Stankiewicz (ICALP, 2019)

Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems). - Manuel Bodirsky; Antoine Mottet; Miroslav Olsák; Jakub Oprsal; Michael Pinsker; Ross Willard (LICS, 2019)

Topology is relevant (in the infinite-domain dichotomy conjecture for constraint satisfaction problems). - Manuel Bodirsky; Antoine Mottet; Miroslav Olsák; Jakub Oprsal; Michael Pinsker; Ross Willard (CoRR, 2019)

Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures. - Libor Barto; Michael Kompatscher; Miroslav Olsák; Van Trung Pham; Michael Pinsker (J. Math. Log., 2019)

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). - Jan Jakubuv; Karel Chvalovský; Miroslav Olsák; Bartosz Piotrowski; Martin Suda 001; Josef Urban (IJCAR (2), 2020)

Property Invariant Embedding for Automated Reasoning. - Miroslav Olsák; Cezary Kaliszyk; Josef Urban (ECAI, 2020)

GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry. - Miroslav Olsák (ICMS, 2020)

ω-categorical structures avoiding height 1 identities. - Manuel Bodirsky; Antoine Mottet; Miroslav Olsák; Jakub Oprsal; Michael Pinsker; Ross Willard (CoRR, 2020)

Loop conditions for strongly connected digraphs. - Miroslav Olsák (Int. J. Algebra Comput., 2020)

Fast and Slow Enigmas and Parental Guidance. - Zarathustra Amadeus Goertzel; Karel Chvalovský; Jan Jakubuv; Miroslav Olsák; Josef Urban (FroCoS, 2021)

Learning to Solve Geometric Construction Problems from Images. - Jaroslav Macke; Jirí Sedlár; Miroslav Olsák; Josef Urban; Josef Sivic (CICM, 2021)

Planning from Pixels in Environments with Combinatorially Hard Search Spaces. - Marco Bagatella; Miroslav Olsák; Michal Rolínek; Georg Martius (NeurIPS, 2021)

Learning Theorem Proving Components. - Karel Chvalovský; Jan Jakubuv; Miroslav Olsák; Josef Urban (TABLEAUX, 2021)

The Role of Entropy in Guiding a Connection Prover. - Zsolt Zombori; Josef Urban; Miroslav Olsák (TABLEAUX, 2021)

Erratum: Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures. - Libor Barto; Michael Kompatscher; Miroslav Olsák; Trung Van Pham; Michael Pinsker (J. Math. Log., 2021)

Maltsev conditions for General Congruence Meet-semidistributive Algebras. - Miroslav Olsák (J. Symb. Log., 2021)

The Isabelle ENIGMA. - Zarathustra Amadeus Goertzel; Jan Jakubuv; Cezary Kaliszyk; Miroslav Olsák; Jelle Piepenbrock; Josef Urban (ITP, 2022)

Machine Learning Meets The Herbrand Universe. - Jelle Piepenbrock; Josef Urban; Konstantin Korovin; Miroslav Olsák; Tom Heskes; Mikolas Janota (CoRR, 2022)

MizAR 60 for Mizar 50. - Jan Jakubuv; Karel Chvalovský; Zarathustra Amadeus Goertzel; Cezary Kaliszyk; Mirek Olsák; Bartosz Piotrowski; Stephan Schulz 001; Martin Suda 001; Josef Urban (ITP, 2023)

Alien coding. - Thibault Gauthier; Miroslav Olsák; Josef Urban (Int. J. Approx. Reason., 2023)

The IMO Small Challenge: Not-Too-Hard Olympiad Math Datasets for LLMs. - Simon Frieder; Mirek Olsák; Julius Berner; Thomas Lukasiewicz (Tiny Papers @ ICLR, 2024)

Graph2Tac: Online Representation Learning of Formal Math Concepts. - Lasse Blaauwbroek; Mirek Olsák; Jason Rute; Fidel Ivan Schaposnik Massolo; Jelle Piepenbrock; Vasily Pestun (ICML, 2024)

Symbolic Computation for All the Fun. - Chad E. Brown; Mikolas Janota; Mirek Olsák (PAAR+SC²@IJCAR, 2024)

Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving. - Jason Rute; Miroslav Olsák; Lasse Blaauwbroek; Fidel Ivan Schaposnik Massolo; Jelle Piepenbrock; Vasily Pestun (CoRR, 2024)

Hashing Modulo Context-Sensitive 𝛼-Equivalence. - Lasse Blaauwbroek; Miroslav Olsák; Herman Geuvers (Proc. ACM Program. Lang., 2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO. - Chad E. Brown; Karel Chvalovský; Mikolás Janota; Mirek Olsák; Stefan Ratschan (CADE, 2025)

Invariant neural architecture for learning term synthesis in instantiation proving. - Jelle Piepenbrock; Josef Urban; Konstantin Korovin; Miroslav Olsák; Tom Heskes; Mikolás Janota (J. Symb. Comput., 2025)

Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. - Yuri Chervonyi; Trieu H. Trinh; Miroslav Olsák; Xiaomeng Yang; Hoang Nguyen; Marcelo Menegali; Junehyuk Jung; Vikas Verma; Quoc V. Le; Thang Luong (CoRR, 2025)