On July 2, 2026, Mistral AI open-sources Leanstral 1.5 — a dedicated Agent for the Lean 4 proof assistant, under Apache-2.0 license, free to use. It uses a 119B-total / 6B-activated MoE architecture, bringing the "small activation, large capacity" paradigm to serious formal mathematics. The scorecard is hard: miniF2F validation/test both saturated at 100%; PutnamBench solved 587/672, 7 more than Seed-Prover 1.5 high, with single-problem cost only about $4 (versus about $300); FATE-H 87 problems, FATE-X 34 problems both rank first on their leaderboards. On the companion open-source FLTEval benchmark, pass@8 climbs to 43.2, surpassing closed-source Opus 4.6's 39.6, at only 1/7 the cost. The training pipeline takes the three-stage path "continued pretraining → SFT → CISPO RL", with RL running on both multi-turn Lean verification environments and code-Agent environments. The most amazing is test-time scaling: PutnamBench Pass@8 climbs monotonically with token budget from 50k to 4M, 44 → 244 → 493 → 587; the AVL tree O(log n) proof ran 2.7M tokens, 22 rounds of context compression, an extreme sample of this curve. On the practical level, scanning 57 real Rust repositories, the model caught 47 suspicious properties, 11 real bugs, 5 of which were never reported on GitHub — including integer overflow in the varinteger library's zigzag decoding at u64::MAX, hard to even hit with fuzzing. Commentary: the real signal isn't the leaderboard, but the "6B activation + complete RL toolchain + Apache-2.0" combination making serious formal verification an engineering base that can be deployed outside of research institutions for the first time. From now on, math reasoning, critical code auditing, and formal security verification teams all have an open-source base that won't be choked by API costs.