Leanstral 1.5

	Leanstral 1.5(docs.mistral.ai)
	259 points by vetronauta 16 hours ago \| 106 comments
	tl;dr: Leanstral 1.5 is an updated Lean 4 formal proof engineering model tuned for automated theorem proving and autoformalization, with 119B total parameters (6.5B active) and a 256k context window. It's offered at no cost and supports a broad feature set including chat completions, function calling, structured outputs, FIM, embeddings, and OCR/document QnA.
	HN Discussion: ↓Frustration with Mistral's product usability, broken pages, and lack of customer support ~Confusion about open-weights claims and inability to find downloadable model weights ~Lament that EU has no competitive SotA LLM offerings despite this release ↑Enthusiasm about Lean 4 focus and integration with existing theorem proving tools •Question why the model specializes only in Lean 4 and not other proof assistants like Coq