We have to remember that OpenAI wanted us to believe that an adversarial AI hacked Huggingface because it was "too ambitious". Then an AI found a proof of Fals

We have to remember that OpenAI wanted us to believe that an adversarial AI hacked Huggingface because it was "too ambitious". Then an AI found a proof of False, hidden in the "proof" of the Collatz conjecture. On the other hand we are supposed to believe that all Astra math results with no independent peer review are correct. The Lean proofs are tens of thousands of lines long with no comments where the main theorem even is. The ambitious AI could have inserted another obfuscated proof of False or hidden False in the hypotheses of the main theorem, wherever that is. Lean, due to its advanced features, has had the most of soundness bugs of all provers: https://cr.yp.to/proofs.html https://cr.yp.to/proofs.html The semiconductor industry uses ACL2 or HOL-light.