Leanstral

Leanstral is a niche tool with an unusually specific audience, which is why it's a listing rather than a full entry: if you know what Lean 4 is, you already know whether you want this model, and if you don't, this model isn't for you. For the curious: Lean 4 is a proof assistant — a programming language that lets you write code alongside machine-checkable mathematical proofs that the code does what it claims. Formal verification is the gold standard for correctness (used in cryptography, aerospace, and verified kernels) but it's historically been too labor-intensive for most software. Leanstral is Mistral's attempt to automate the hard part.

What makes this listing notable beyond the niche itself: (1) it's the first open-sourceA stricter standard than open-weight: the weights, the training code, and the training data are all released publicly. Very few large language models meet the full open-source bar — most "open" models in the AI world are actually open-weight. When in doubt, check the license file and the creator's documentation. formal-proof agent — previous tools in this space were either research prototypes or wrappers around closed-source models; (2) it's derived from Mistral Small 4 and inherits the 6B-active MoEA model architecture that splits the model into many smaller specialized "expert" networks, only activating a handful per input rather than running the whole model every time. The practical effect: you get the knowledge capacity of a big model with the compute cost of a much smaller one. Mistral Large 3 and Mistral Small 4 are both MoE models. efficiency, which is why Mistral can price it at ~1/15th the cost of Claude Sonnet on equivalent proof tasks; (3) the Apache 2.0 license here is genuinely unrestricted, unlike the custom license that covers the 123B Devstral 2 flagship. For Lean 4 developers in research, cryptography, or formal methods work, this is a materially new tool. For everyone else, it's a signpost that formal verification is becoming AI-accessible.

Deployment: free API endpoint labs-leanstral-2603 for evaluation, Mistral Vibe CLI integration (/leanstall command), or self-hostedRunning a model on hardware you control — your own servers, your own cloud instance, or your own laptop — rather than paying to access it through someone else's API. Self-hosting gives you full control over data and predictable costs, but requires the hardware and operational effort to run the model. Only possible with open-weight models. on vLLM with 4× GPUThe specialized chip that runs most AI models. Originally designed for 3D graphics, GPUs turned out to be excellent at the math AI requires. Nvidia dominates the AI GPU market; common datacenter models include the H100, H200, and B200. Running an AI model without a GPU is possible but painfully slow for anything but the smallest models. tensor parallelism. See the model cardThe documentation that ships with a model, typically on Hugging Face or the creator's site. A good model card lists the architecture, training data summary, intended uses, limitations, evaluation scores, and license. Model cards are the catalog's primary source for listing entries; each catalog entry links back to the canonical model card. for configuration details.