Leanstral 1.5 119B A6B GGUF This repository contains the GGUF quantized version ( Q4 K M ) of mistralai/Leanstral 1.5 119B A6B. Leanstral 1.5 is an open source code agent model designed for Lean 4, a proof assistant capable of expressing complex mathematical objects such as perfectoid spaces and software specifications like properties of Rust fragments. Built as part of the Mistral Small 4 family, it combines multimodal capabilities and an efficient architecture, making it both performant and cost effective compared to existing closed source alternatives. [!Note] This is an updated model of the previously released Leanstral model. Key Features (Base Model) Leanstral incorporates the following architectural choices: MoE : 128 experts, 4 active per token Model Size : 119B parameters with 6.5B activated per token Context Length : 256k tokens Multimodal Input : Accepts text and image input, producing text output Recommended Settings Temperature : 1.0 Reasoning Effort : 'none' → Do not use reasoning 'high' → Use reasoning (recommended for complex prompts). Context Length : ≤ 200k tokens recommended Local GGUF Deployment Because this is a GGUF file, you can run it locally using llama.cpp…
We use cookies for essential functionality and analytics. You can accept or reject analytics cookies.Cookie policy