Excellent point. What mathematicians write to each other are arguments not proofs. Machine checkable proofs are really proofs.

This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and proofs can be improved. Tools for each can be developed without having to support both.

What is the philosophical difference between an 'argument' that human minds following the laws of logic agree on "is correct" and a machine built by these minds flashing a "correct light"?

IMO the only advantage to be gained by introducing physical computers in the picture is lightning-fast book keeping.

Why would you trust an Intel CPU, a Samsung SSD and a linux fs driver running some verifying framework more than the human brains designing, writing and executing said framework?