Matěj Kripner

I'm a PhD student at ÚFAL at the Faculty of Mathematics and Physics, Charles University in Prague, advised by Milan Straka and Martin Schmid. Currently I'm a research intern at Google Zürich, working with Goran Žužić.

I work on applied reinforcement learning in robotics, computer vision, and automated theorem proving.

Email GitHub Google Scholar @MatejKripner

Publications

NanoProof: Factorized Execution-Guided Proof Search in Lean 4

Matěj Kripner, Milan Straka

Under review

Code

From Expert-Guided Proof Search to Automated Open-Problem Solving

Martin Balko, Jan Grebík, Pavel Hubáček, Martin Koutecký, Matěj Kripner, Václav Rozhoň, Robert Šámal, Adrián Zámečník

MATH-AI Workshop @ NeurIPS 2026

Bolzano: Case Studies in LLM-Assisted Mathematical Research

Martin Balko, Jan Grebík, Pavel Hubáček, Martin Koutecký, Matěj Kripner, Václav Rozhoň, Robert Šámal, Adrián Zámečník

Technical report

Paper Web Code

OpenProver: Agentic and Interactive Theorem Proving with Lean 4

Matěj Kripner, Milan Straka

Conference on Intelligent Computer Mathematics (CICM 2026)

Paper Code

LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

Matěj Kripner, Michal Šustr, Milan Straka

AI4MATH Workshop @ ICML 2025

Paper Code

Symbolic World Models in Lean 4 for Reinforcement Learning

Matěj Kripner

Programmatic RL Workshop @ RLC 2025

Paper Code

Learning to Summarize Without Human Feedback via Reference-Free Token-Level Reward Function

Matěj Kripner

Master's thesis

Emergence of Novelty in Evolutionary Algorithms

David Herel, Dominika Zogatová, Matěj Kripner, Tomáš Mikolov

Conference on Artificial Life (ALIFE 2022)

Paper

Posts

Playing Chess with an SO-101 Robot Arm

Teaching π0.5 to play physical chess with the SO-101 robot arm: How I got to a working demo and what is planned next.

Papers Week

Reading five papers in five days: Kimi K2.5, DeepMind’s work on AI4MATH, QED-Nano, Numina-Lean-Agent, and I-JEPA.

Let's see how TRM reasons

Looking inside the Tiny Recursive Model’s latent recursion traces on ARC, with the hypothesis that its intermediate states decompose a task into reusable concepts.

Paper notes: σ-GPTs, A New Approach to Autoregressive Models

σ-GPTs generate a sequence in any order, not just left to right — two small changes to a standard GPT, and a rejection-sampling trick that fills in many tokens per pass.

Paper notes: Longformer, The Long-Document Transformer

Longformer replaces full self-attention with a sliding window plus a few global tokens, cutting the quadratic cost down to linear in sequence length.

Paper notes: Reasoning over Paths in Knowledge Bases using Reinforcement Learning

MINERVA answers knowledge-graph queries by learning to walk the graph: a policy-gradient agent that picks one outgoing edge at a time instead of enumerating every possible path.

Publications#

Posts#

Publications

Posts