by Grimblewald
15 subcomments
- 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?
by henryrobbins00
0 subcomment
- 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
by helloplanets
10 subcomments
- Tangential, but I'm pretty sad about EU having absolutely nothing in the actual SotA LLM market. Especially given the recent events of US completely restricting the actual SotA models.
Has this been just pure lack of funding and infra?
- 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
- 404?
https://web.archive.org/web/20260630223430/https://docs.mist...
- Discussion about Leanstral 1: https://news.ycombinator.com/item?id=47404796
- "Page not found" for me. Did you manage to access this? What is this about?
- Lean 4 and Idris 2 are underrated, and likely great for LLM's to code in (since they provide additional guarantees)
- I am getting 404 right now
by impodimium
1 subcomments
- Interesting that this only specialized for Lean4 and not for similar like Coq
by doctorpangloss
17 subcomments
- 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.
- Registered due this news. But I must connect to GitHub to use "Code"? That seems limited?
- Is this useful for specifying programs too or only theorems?
- [dead]
- This went to market horribly (if you can even call it that), just look at the comments. Mistral played themselves big time over the past ~18 months. Non-competitive products and models combined with bad marketing and GTM...Oh Europe
Hacker News