---
title: "Lean"
description: "1 posts about Lean, summarised, each linking to the original."
---

# Lean
> 1 posts about Lean, summarised, each linking to the original.

## Articles

### [Building an RL theorem-proving workflow on Modal](https://yomu.fyi/post/building-an-rl-theorem-proving-workflow-on-modal.md)
- Company: [Modal](https://yomu.fyi/company/modal.md)
- Published: Apr 29, 2026
- Type: Explainer

AE Studio built a distributed reinforcement learning pipeline on Modal to train LLMs to prove theorems in Lean. They compared Group Relative Policy Optimization, which groups attempts and applies gradient updates, with Evolution Strategies, which evaluates a population of perturbed models and updates based on success rates. The workflow used Modal’s per-function images to separate a vLLM instance on GPU for proof generation, CPU-based Lean verification, and orchestration, with .map() fanning out runs and Sandboxes isolating verification batches. ES enabled stateless checkpointing via seed histories: each worker loaded base weights from a Volume, replayed past seeds and rewards (about 200 bytes per iteration), and reconstructed the model on GPU without transferring large weight files. Early results on the lean\_workbook dataset using the Kimina-Prover-Preview-Distill-1.5B model showed ES matching or outperforming GRPO in verified proofs per iteration, especially with limited data, though gains varied.