Hacker News

i would argue it is more valuable

I'm not sure the "a year of document processing for under 100 USD/y" is such as great thing as you think it is (at least not for European competitiveness)... It means Mistral is essentially setting a revenue ceiling very low. OCR is a commodity at this point, and open source models, AWS, etc already do it out of the box.

Plus, you can't really build loyalty on a 100 USD/Y price tag. Since there are no switching costs holding them back, those buyers will leave the moment somebody offers a lower rate. An easily cloned, low cost tool with zero customer lock in is not a business. It is a feature.

That might sound great for the buyer (you), but it is a terrible strategy if we want a European company to compete long term against global competitors on actual product merit instead of just regulatory arbitrage.

But how does it compete on OCR? I find that having good quality at a cheap price is more niche than having the best quality at 10x the cheap price, because for most use cases you want to pay a bit more if it saves you mistakes later.

Stupid Europoors, optimizing for making a good product, instead of optimizing for making as much money as possible /s

particularly "and fuzzing", yea. fuzzing generally does intentionally explore boundary values, from what I've seen. for an encoding library like this, I think it's fair to say that fuzzing is a baseline expectation for any decent code, and it almost certainly would've caught this in seconds.

--- edit

concretely, I made a very simple round-trip test with proptest, and got dozens of failures and this in less than a second:

    thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
    Test failed: attempt to multiply with overflow.
    minimal failing input: value = 4611686018427387904
        successes: 2
        local rejects: 0
        global rejects: 0

Maybe it's not something they would "typically miss", but, from proof by existence, it's something they sometimes miss.

It does speak to the benefits of using lean in that you don't need to be clever about the different examples you test.

Yes, it's basic QA. If tests missed this kind of thing, they would be of much more limited use than we generally expect them to be. It raises questions about the authors' background.

Because this is garbage PR. That's it.

Every property-based testing system (invented ca. 1980) will explore boundary values. The semantics (or lack thereof) of C and C++ can make this difficult to actually test for because the compiler is allowed to say "test passed" to any input leading to UB.

It’s a 6bn model. Totally different class. I’m more excited about “frontier small language models” tbh.

Agreed, though open weights + relatively small is still headline worthy. This thing really cooks.

The problem with proof is that it’s a bit hard sometimes to convey the value. The point is not to find bugs, but to prove that there are none (of a certain class; under certain assumptions; etc). But it’s a hard story to sell, so often the marketing is around “look at this bug we found”.

You need to understand the bits you are trying to prove, but not the full proof. It's more like reading haskell types than math, even though the vocabulary is heavily inspired by math.

Read this section of the article “ Bug Discovery: Finding Hidden Flaws”, they appear to have used the model on open source Rust to find issues starting with just the Rust code. You might be also able to have conversations that help you write the Lean to verify your application, but I’m not certain about this.

I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.

I've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4.

I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore.

The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense.

It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.

It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.

However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.

Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.

Have you ever been downvoted for calling 'dupe?' I once was downvoted after calling dupe on a link posted thrice. HN is an interesting place to hang out, that's for sure.

> It also found the bug that Leanstral 1.5 found and the authors highlighted

This is a little bit like someone pointing the moon and you look at the finger.

The formal proof domain goes way beyond just finding bugs.

It has tons of usages in term of functional safety, protocol validation, cryptography, etc...

The fact Mistral tackle this kind of problem is both smart and not so surprising.

Smart because it is niche enough that they do not front face the big competitors (yet).

No so surprising because the French labs have a well known and long time expertise with formal proof tools (Coq and all its Ocaml associated tools). It has been historically mainly pushed by the aerospace and train industries (Airbus, Dassault, Alsthom).

Given that they directly compare to GPT-5.5 in their documentation. This comes off as puppy kicking to me. They state it is not SOTA, even IN its domain!

Honestly: Think twice before dragging your firm into what you say.

Disclaimer: I speak for myself. Not any firm I am associated with.

Leanstral 1.5 has 6B active parameters. How many parameters does GPT-5.5 have?

GPT-5.5 is what, a trillion+ parameter model? I think the insight here is that you can do this with a tiny model.

the mechanism is whats interesting, rather than whether it could do it.

this sounds like a great tool to add to the toolbelt, as part of the "how do we handle all the code output from LLMs" problem

At this point I wouldn’t move to USA if you paid me double the salary. There are more things in life than money.

That said, if (or when) the progress of the LLMs flatten out, then I think even Europe can catch up in a few years. If they don’t, and that seems unlikely to me, if the required compute needs to increase at the rate it does today, then I am not sure any of us can predict where society ends up.

Fortunately for Europe, the US is doing its best to make itself both an undesirable and unavailable immigration target.

treated far better != earn more money

As somebody who moved to the US and then back to Europe again, you may get more money there, but you'll pay for it with a much worse environment and lifestyle.

Life's not all about the number on your bank account. Once you're past a certain level (which a competent engineer can easily reach in Europe as well), the marginal utility of money diminished quite quickly.