Language Modelling and Scaling Laws for Lean’s Lambda Calculus

Typed lambda calculi underlie many proof assistants; e.g., Lean’s kernel checks terms that express proofs and programs, making proof steps explicit. How difficult is this language for an autoregressive model to learn and generate? We compare kernel terms, surface Lean, and informalised English descriptions of the same Mathlib theorems using our developed serialisation method, which follows the dependent type from left to right. The decoder then samples kernel expressions, which can be checked without elaboration. We probe the scaling laws, both from scratch and with a warm start using Qwen3, in each language. For Qwen3-4B warm starts under reference prefixes, the 1% of proof tokens with the highest loss carry 98.6% of term proof loss, against 10.7% for surface Lean and 14.3% for English. Mean term proof loss is 2.475 times surface Lean’s at these warm starts but falls faster with model size and data from scratch, though the grid’s single learning rate slightly inflates the term model-size exponent. If the fits continue with fresh data and model size taken to infinity, term proof loss crosses below surface Lean’s after about 7 times the current pool of distinct proofs. The transferred Qwen3-0.6B achieves a term proof loss lower by a factor of 3.68 than the same network trained from scratch on the same number of tokens. Based on these results, we’re in a position to use pretrained models and increase the dataset size for kernel term language.