TX_044· AI
Mistral's Leanstral writes machine-checkable proofs in Lean 4
Mistral released Leanstral on March 16 — the first open-source AI agent built specifically for Lean 4 formal proof engineering. Generates code plus a machine-checkable proof of correctness.
