Leanstral 1.5

Original Article ↗ Hacker News Discussion ↗

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.