“There’s a perception of mobster behavior” from leading AI companies, one mathematician tells WIRED as OpenAI prepares to release more than 100 new solutions to unsolved problems.
having a Lean Theorem/Proof only proves they are connected to the axioms
Lean is not enough to personally verify the proof. We can see that even now with the stolen C+D Navier proof, where OpenAi paper - as we know since yesterday - is… possibly false (well, we know that the lean code does not match the paper, let the mathematicians cook).
The proofs are written in Lean so, like in all mathematics, you don’t have to trust the person because you can independently verify the proof.
That’s not how Lean works.