Leanstral 1.5: Proof abundance for all

	Leanstral 1.5: Proof abundance for all(mistral.ai)
	370 points by programLyrique 49 days ago \| 103 comments
	tl;dr: Leanstral 1.5 is an Apache-2.0 licensed model (119B total/6B active params) for Lean 4 proof engineering that saturates miniF2F, solves 587/672 PutnamBench problems at ~$4 each (vs. ~$300 for Seed-Prover), and sets SOTA on FATE-H/X. Trained via mid-training, SFT, and RL with CISPO across theorem-proving and code-agent environments, it also demonstrated real-world utility by uncovering 5 previously unknown bugs across 57 open-source repositories. Weights are on Hugging Face with a free API endpoint available.
	HN Discussion: ↑Mistral's focus on efficient specialized models is valuable even if not frontier-competitive ↓The highlighted bug-finding example is unimpressive as testing would catch such boundary conditions ↓Benchmark comparisons use outdated competitor models, making claims less impressive •Questioning why Lean 4 was chosen over other formal verification tools like Isabelle/HOL or TLA+ •Curious whether the tool is accessible to newcomers without formal verification background