Leanstral 1.5: Proof abundance for all

	Leanstral 1.5: Proof abundance for all(mistral.ai)
	270 points by programLyrique 14 hours ago \| 79 comments
	tl;dr: Leanstral 1.5 is an Apache-2.0 licensed Lean 4 proof model (119B total/6B active params) that saturates miniF2F, solves 587/672 PutnamBench problems at ~$4 each (vs. ~$300 for Seed-Prover), and sets new SOTA on FATE-H/X. Trained via mid-training, SFT, and RL with CISPO across multiturn and code-agent environments, it also demonstrates real-world utility by finding 5 previously unknown bugs across 57 repositories and proving O(log n) complexity for AVL trees. Weights and a free API are available on Hugging Face.
	HN Discussion: ↑Mistral's niche of high-quality specialized small models is valuable despite not competing with frontier models ↓The highlighted bug-finding example is unconvincing since testing/fuzzing would easily catch that boundary case ↓Benchmark comparisons use outdated competitor models, making the SOTA claims less impressive •Questions about practical accessibility for non-Lean users and choice of Lean 4 over Isabelle/TLA+ ↑Enthusiasm for Lean and the release, with interest in integrating it into existing tools