Remix.run Logo
▲ perching_aix an hour ago

> Couldn’t the Lean code just be formulated incorrectly?

I believe so, even with all the usual safeguards properly in place: https://news.ycombinator.com/item?id=49672339

> is everyone just assuming that it just be true because the Lean code checks out?

Kinda? It's only been 24 hours since they dumped 722 manuscripts on the world, most of which are apparently basically unreadable, and only some of which come with a Lean proof, which in itself is not a joy to read afaik.