Morning Edition · Sunday, July 5, 2026Published at 6:42 AM EDT · New York

Mistral Updates Leanstral, Its Model for Machine-Checked Proofs in Lean 4

Version 1.5 targets formal verification, where a compiler, not a benchmark, decides whether the answer is correct.

Mistral has released Leanstral 1.5, an updated version of its model for formal verification in Lean 4, according to AI ML Big Data. Lean 4 is a proof assistant, software that checks mathematical proofs. The model's job is to help write and…