erichocean

> we will hit Godel

It seems no one understands how useless this theorem is in practice.

both

What he is calling "vibemathing" is actually just engineering.

Engineers don't have to know why something worked in particular in order to use it, they just do.

Science later tries to figure that out.

Both are valuable, but the idea that science must be "first" is, at best, unsupported by the evidence.

I do not encourage you to look at the diagonalization argument, it has similarly uncomputable elements (that take "longer than infinite" time because they are unconstructable).

You've lost the plot.

Not once have I said "Mistral should not train models."

I have questioned doing yet another useless pretraining on a pre-existing, non-innovative model backbone.

Mistral spends their money and GPU time poorly, and the results demonstrate just that.

It's science (understanding) before engineering (efficacy).

The most common Science™ failure mode.

You do realize that China is not the only place making open weights models, right?

> they'd be unable to justify their valuation or investments

I don't think they're justified now, certainly their results don't justify it. Mistral is mid at best.

> It's core to their whole value proposition that they are providing sovereign AI capabilities in Europe.

Except they don't, they are dependent on GPUs from nVidia and AMD—both American companies.

> high-quality open source model

> that isn't owned

I don't know what definition of open weights you are using, but the "open" part is what allows you to use it without being beholden to American Trillion-dollar companies or the Chinese.

Mistral could do exactly what Cursor does, and post-train the model to meet the needs of Europeans.

That's a far more efficient (and useful!) use of GPUs than yet another pretrain on an outdated model backbone.

Sure, agreed. But they do their own pre-training, at great expense, on outdated model backbones.

Wouldn't it be better to do something more like Cursor, and RL on an existing pretrained model if you're not innovating anyway?

Yes, actually. Thanks for asking.

It's not any more difficult to build and run a JAR, either.

And compared to Go, the production observability is very good.

I also use Clojure and can observe my running app with a full REPL.

> which Mathlib coalesced as a side-effect of it's capability

Eh, Lean was heavily developed based on feedback from mathematicians; it's not a side-effect but more like a "driving force."

Source: one of Lean's co-authors.