Leanstral 1.5 makes formal proofs more accessible

Mistral introduced Leanstral 1.5, a model with six billion active parameters released under Apache 2.0. The team reports improvements on formal-verification benchmarks and examples of discovering bugs in repositories. The release includes open weights and an API route for working with Lean 4.

Context

Formal verification has an unusually valuable feedback mechanism: a proof checker can reject an invalid argument. That does not make every useful theorem easy to formulate. The human task includes choosing what to prove and confirming that the formal statement actually expresses the intended property.