Job Petrovčič: Kernel-level expression generator

Abstract: We introduce a neural generator that produces valid Lean 4 expressions directly at the kernel level, bypassing Lean's elaboration process. To train the generator, we implement Lean's core type checking in Python and integrate it into a reinforcement learning environment that assigns rewards for well-typed subexpressions. As the standard formulation of reinforcement learning is insufficient for discovery, we integrate the concept of surprisal to enhance the model's exploratory behaviour. We evaluate the model's ability to explore the environment with surprisal-driven training and compare this approach against baselines.