We pretty much crossed this bridge in 1976 with the proof of the four-color theorem: https://en.wikipedia.org/wiki/Four_Color_Theorem
The process of automating mathematics:
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)
The process of automating mathematics:
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)