This is quite interesting, especially since one of the major objections to computer-aided proofs has that they are more difficult for humans to understand.
Common wisdom has been that proof techniques matter more than the results, but if human-authored proofs are no longer being inspected, it seems like it's just a matter of time before computer-aided proofs take over. I wonder how long it will be before proof assistants (like Lean, Coq, etc.) become ergonomic enough that the average non-technical math researcher will feel social pressure to publish a computer-aided proof along with their result.
Common wisdom has been that proof techniques matter more than the results, but if human-authored proofs are no longer being inspected, it seems like it's just a matter of time before computer-aided proofs take over. I wonder how long it will be before proof assistants (like Lean, Coq, etc.) become ergonomic enough that the average non-technical math researcher will feel social pressure to publish a computer-aided proof along with their result.