thejokeisonme

Due diligence?

Re aside: Ok, but consider that maybe it is rude to ask people to read something you didn't write without warning. I'd add a disclaimer whenever I post about it, and on the very top of the readme. Better: have a readme for humans that you wrote, and leave the current document as a readme for machines.

Yeah, it's so funny seeing all these people discover Lean as if it invented mechanizing mathematics. Even Coq wasn't the first (might have been the first with dependent types though).

Putting aside the Claudisms.

You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.

Not saying your niche doesn't have value, but you can get interesting ideas from there.

No, this isn't what this is about. From the abstract:

> In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully.

They claim that each solution only needed 3 hours on the next generation public model, iiuc. So this theory doesn't really hold up.

A lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.

How would these ideas be available to steal?

You emphasize TWO as of these kernels are so different.

Was your understanding of language also impaired?

How can you scrutinize something you don't understand?

Same!

This doesn't make any sense! Arguing for the sake of arguing.

Why is Windows not open source then, where we can trust Microsoft based on the experience with previous Windows versions?

> going on pure trust

The trust in open source software is founded on the process which involves people being able to understand the code given they have the right expertise. I don't see how this process works with open weights.

Having zero knowledge about these studies I have high credence they are baloney.