Job Petrovčič
MSc Mathematics, University of Ljubljana · Ljubljana, Slovenia
About
I work at the intersection of machine learning and formalised mathematics: graph neural networks for premise selection in Lean 4, and a from-scratch Python reimplementation of the Lean kernel as a reinforcement learning environment. IMO bronze medallist, two-time IMC First Prize.
MSc Mathematics at the University of Ljubljana (GPA 10/10); BSc 2023 (GPA 9.87/10, Prešeren's Prize). Erasmus semester at TU Munich, 2026.
Publications
-
Combining Textual and Structural Information for Premise Selection in Lean
J. Petrovčič, D. E. Narváez, L. Todorovski · 5th MATH-AI Workshop, NeurIPS 2025
-
Kernel-level expression generator
J. Petrovčič, S. Mežnar, L. Todorovski · EuroProofNet WG5 Workshop, Edinburgh, April 2025
-
Sequential DAG Generation
J. Petrovčič, S. Mežnar, L. Todorovski · 17th Jožef Stefan IPS Students' Conference, 2025
Projects
- Artin–Wedderburn in Lean 4 — formalisation of the theorem with Matevž Miščič and Maša Žaucer; blueprint, docs and code.
- LeanPy — the Lean 4 kernel reimplemented in Python, and an RL environment built on it.
- GNNReProver — graph neural networks for premise selection inside the LeanDojo/ReProver pipeline.
- agda-unimath Library Explorer — visualisation tool for the Agda-Unimath library.
Talks
- Slovenian Network Analysis Researchers' Meeting, Ljubljana —
- IPSSC Students' Conference, Kamnik —
- EuroProofNet WG5: Theorem Proving and Machine Learning in the Age of LLMs, Edinburgh —
- Seminar for Foundations of Mathematics and Theoretical CS, Ljubljana —
Awards
- International Mathematical Olympiad 2020 — bronze medal
- International Mathematics Competition for University Students — First Prize, 2023 (41st) and 2024 (96th) of ~400
- Simon Marais Mathematics Competition 2024 — 4th of 55 pairs
- Slovenian University Programming Marathon — champion 2021, 2022, 2023; runner-up 2024
- European Physics Olympiad 2020 — bronze medal
- Prešeren's Prize, UL FMF — for the BSc thesis Diffeomorphisms of Surfaces
- DMFA Scholarship 2025/26 · Zois Scholarship 2016–2026