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…
Leanstral 1.5
61–70 of 158 posts
Re: Leanstral 1.5
#62Earlier quoted context omitted.
OCR is off the charts good on every metric you can think of. LLMs are a near-afterthought at this point if you don’t have data residency requirements. I love them and they’re slightly under rated, their models are consistently well-trained, open, but as you note, behind. There is no metric that will say they’re ahead in anything.
This. Best OCR provider by measure and it’s been for years
Re: Leanstral 1.5
#63Re: Leanstral 1.5
#64Tangential, 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?
[flagged]
Re: Leanstral 1.5
#65Tangential, 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?
[flagged]
Re: Leanstral 1.5
#66Earlier quoted context omitted.
[flagged]
That act applies just as much to those American and Chinese models within the EU.
Re: Leanstral 1.5
#67Tangential, 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?
Re: Leanstral 1.5
#68Tangential, 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?
The only way to avoid this is to stop playing the game as it is today, and start using proper industrial policy to build up a competitive industry (like China did). There has been no appetite for that the last decades, but Trump is making it completely clear that the state is back, and Europe is slowly acknowledging it as well.
Re: Leanstral 1.5
#69"Page not found" for me. Did you manage to access this? What is this about?
Leanstral 1.5 - June 30, 2026 An updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. 119B total parameters, 6.5B active.
https://web.archive.org/web/20260630223430/https://docs.mist...
Re: Leanstral 1.5
#70Tangential, 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?
The EU simply doesn't have a proper common market, especially when it comes to capital. Having more people than the US and a big economy in aggregate doesn't matter much if you can't efficiently pool resources. Could we in Europe have 100 billion fundraises for a new lab? If not, then it's over and you can give up.
But there are other ways to pool resources than the free market. Airbus was not made dynamically in a market, neither was the LHC. 100 billion € is a lot, it's half of the total allocated aid from Europe to Ukraina. Which can be read in two ways, either 'helping Ukraine is already weighing us down, another similar cost is too much for some IT toy ', or 'Europe has the ability to collect massive amount of capital when it needs to, and AI is a existential threat which justifies it'.