Leanstral 1.5
Mistral’s new Leanstral 1.5 model targets formal proof engineering in the Lean 4 theorem prover, prompting debate over its practical value, accessibility and the niche nature of automated theorem proving. Commenters contrast Mistral’s strengths in areas like OCR, speech transcription, latency and pricing with its lagging position in frontier LLM performance, and many note they choose it mainly for EU data residency, regulation, or political reasons. The thread broadens into concerns about Europe’s lack of state-of-the-art AI players, regulatory and funding constraints, and how these shape the continent’s ability to compete with US and Chinese labs.
Model capabilities and use cases
- Several comments praise Mistral models for creative writing: described as having a distinct, “weird” and off‑kilter voice that can be hard to distinguish from humans in an AI-vs-human text game.
- Some users find Mistral Medium better than certain competing frontier models for general writing and for extracting structured info from PDFs and complex schedules.
- Others report weaker coding ability than some smaller/cheaper models (e.g., Gemma, Qwen, Xiaomi MiMo) and consider Mistral “behind” on general LLM metrics.
- Mistral’s OCR and STT/TTS (especially Voxtral Mini and French TTS) are repeatedly described as being at or near the frontier and very cost-effective.
- Some still prefer older/open Mistral models (e.g., Nemo 12B) for summarization style, though often default to other models already loaded locally.
Reasons people use or avoid Mistral
- Positive factors: EU origin / data residency, good API pricing for some workloads, low latency and fast token generation, strong B2B focus, perceived transparency about environmental impact, and responsive human support (for some).
- Negative factors: lack of batch caching (making some workloads ~10x more expensive than Google), perceived weaker performance vs Chinese open models, and absence of clear “best-in-class” metrics for general users.
Leanstral and formal methods
- Leanstral 1.5 is presented as a Lean 4-focused model for automated theorem proving and autoformalization; target audience is formal methods and proof engineering, not general users.
- Discussion connects this to Lean as both a proof assistant and general-purpose language, with mention of real-world use (e.g., Advent of Code).
- Benefits: strong guarantees via Curry–Howard; drawbacks: limited documentation, instability, and a thin ecosystem.
- Some wish for support for other systems (e.g., Coq, Metamath-style explicit proof objects).
- OpenATP, an agentic ATP framework, already integrates Leanstral and will update to 1.5.
Product, access, and support issues
- Multiple users report the Leanstral 1.5 model card returning 404 and being briefly only available via the Wayback Machine.
- Confusion over licensing: docs say Apache-licensed weights, but no obvious download link beyond an older snapshot; status of full weights availability is unclear.
- Some users can access Leanstral as a labs model for free, while others get errors enabling labs and are told self-serve activation isn’t available for standard accounts.
- Experiences with support are mixed: some report prompt replies; others say emails go unanswered and that the help system feels ineffective or “AI-coded.”
EU AI ecosystem and regulation
- Several comments broaden the discussion to EU AI: frustration that Europe lacks true state-of-the-art LLMs, with blame placed on underfunding, fragmented capital markets, cautious regulation (AI Act, GDPR, copyright rules), and cultural factors.
- Counterpoints argue the European tech sector is still substantial; the main gap is in capital scale vs US/China and in political willingness to fund AI at tens-of-billions levels.
- Some see Mistral as sensibly focusing on narrower, winnable niches (e.g., Leanstral, Voxtral, OCR) rather than chasing global frontier models.