Tools

We’ve also been building a couple of projects alongside TorchLean. One helps us understand where our programs spend their time; the other gives us room to explore larger experiments and formalize the ideas behind recent model papers.

Profiling

LeanProfiler

When a Lean program gets slower, we want to know where the time went. With LeanProfiler, we can name the parts we care about, such as loading data, running a forward pass or taking a training step, and measure them as the program runs. We can open the timeline in Perfetto and compare the JSON reports from two runs.

We use it around an existing TorchLean model runner, but it works with other compiled Lean programs too. For asynchronous GPU work, we can wait for the work to finish before closing a measurement. That measures the time until completion; individual kernel timings need a device profiler.

Experiments and proofs

TorchLean Verified Examples

This is where we take a machine-learning question and spend more time with it. Can changing the surrounding batch change a model's answer? Can we export a checkpoint and replay it in Lean? What does it take to train GPT-2 from Lean? The examples bring together code, experiments and proofs so we can work through those questions.

We're also working through the Kimi K3 and Nemotron reports, writing their mathematical definitions with TorchLean tensors and proving properties of those definitions. I'd love to see more model papers explored this way, with the equations, Lean code and explanations together : )