pull down to refresh
Technically, the verification phase does not even require a human anymore with Lean. As long as you believe there are no bugs in Lean (there have been, in the past, so that's a strong caveat), the proof follows from known definitions, axioms, and assumptions. Another caveat is that one can add one's own axioms, so, you'd be able to prove anything if you're not careful and/or dishonest (ouch, maybe yet another reason to be careful with AI-encoded Lean proofs).
reply
Wait, I always thought 2+2=4 no matter how its solved :-)
This is an adjustment period where complicated calculations will be done by AI in 3 min and it will take a human to verify in 3 weeks, and only then we will "declare" as the truth
We as humans do not have brain capacity to compute as fast as machines do, neither we need to (that's why we have them machines) but we still do not fully trust them, hence "we always done it this way" will stay and linger for a while...
"...Our ideas we disseminate in talks, private discussions and careful writeups, connecting them to the previous ideas of others. These processes invariably take time and are based on human interaction...."
'Quite frankly Dear, I don't give a damn' (Thanks Clark) - math is math no matter how you slice it imho.
It's a sentiment we have problems to let it go.
AI is a tool we just need find the proper adjustment and learn how to use it. is all.
My 2 satoshis... YMMV