Leanstral 1.5

__natty__

Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796

doctorpangloss

Real talk, does anyone use anything from Mistral because it performs the best, by whatever secular metric of your choosing? Or is it only used "because EU"? Just focus on answering the question. I wonder if anyone has observed it perform better on any objective metric in any rigorous setting.

esafak

Is this useful for specifying programs too or only theorems?

impodimium

Interesting that this only specialized for Lean4 and not for similar like Coq

henryrobbins00

What a coincidence! I just released OpenATP earlier today. OpenATP is an open-source Python package and CLI for agentic automated theorem provers. It includes support for Leanstral with Mistral’s Vibe harness. The previous production Leanstral model was deprecated on May 22nd. I will update the package to point to Leanstral 1.5 ASAP! GitHub: https://github.com/henryrobbins/open-atp Docs: https://open-atp.henryrobbins.com

pmarreck

Lean 4 and Idris 2 are underrated, and likely great for LLM's to code in (since they provide additional guarantees)

Grimblewald

Got curious, sign up, add money to account, try to use. Can't, it's a labs model. Fine, let's enable labs. Can't, unspecified error. Fine, lets contact customer support as instructed, can't no customer support, just a half-assed FAQ, that seems vibe-coded and searched poorly, totally irrelevant answers coming up for all queries tried. Then it hit me: If AI makes good customer support, then why does no AI company use theirs to provide customer support?

c7b

I'm not sure I understand the Weights policy. This site says the weights are Apache-licensed, suggesting it's open weights. But I can't find a download link. Their Huggingface profile seems to only provide an earlier snapshot [0]. Any pointers on whether/where we can or will be able to download the weights? [0] https://huggingface.co/mistralai/Leanstral-2603