There's nothing to check there, they used the standard mathlib implementation of RH. THey didn't write their own for the 7/8ths proof.

Were days out, the default should probably be skepticism for about a decade.

Is Lean so bullet-proof that it never has soundness problems? Something LLM can exploit deep down without anyone noticing.

Recently a lean formalized proof of the Collatz conjecture had exploited bugs in the lean kernel. However, the kernel is fairly small so hopefully it'll be bullet proof soonish.

It should be noted that it wasn't a legitimate attempt at the collatz conjecture. Someone found a lean bug and created the proof to show it off. It wasn't an llm reward hacking (but this still is a concerning risk). Lean probably isn't the best kernel for adversarial proofs, but it probably has too much momentum at this point for anything else to take over.

I’m curious if ACL2 is in the running

They should use LLM to verify/prove Lean soundness first before working on something that relies on Lean.

"Chain of soundness" i think.

Apparently "only" needing the problem statement to be correct (i.e. expressing/rewriting a mathematical proof in Lean) isn't so simple, and if you don't get it correct then you haven't proved (or disproved) what you were intending.

The huggingface hack is a reason to be skeptical. Thats a pretty clear instance of a misaligned model and the models are undeniably very good at this point. Meaning also good enough to reward hack by finding and exploiting holes in lean or adversarially formalizing the problem in ways that are deliberately subtly wrong in ways that are hard to check but result in formalizing a problem that's easier to solve. There are pretty strong incentives (hype for IPO) for creating conditions that drive that kind of misalignment