Hinestly, AI can be a great tool to further evolve mathematics,but you still have to understand every gory detail it did to solve the problem. If you can’t do that, it’s not solved.
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).
Hinestly, AI can be a great tool to further evolve mathematics,but you still have to understand every gory detail it did to solve the problem. If you can’t do that, it’s not solved.
Also all ML models have some accuracy less than 100%, that means you can’t trust it. The whole point in the proof is perfection
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.
deleted by creator