Tom Hales discussed formalizing modern mathematics, possibly all of modern mathematics, and proposed that mathematicians enter theorem statements in a formal language without necessarily translating their proofs.

“He, he was talking about formalizing modern mathematics, you know, perhaps all of modern mathematics. Uh, and one of the things he suggested was that perhaps it was time, uh, that we got mathematicians not to learn enough about these computer theorem proving languages to actually type in all their proofs, but just to literally type in the statements of their theorems, because that's a much easier job just saying, "Okay, I claim that I've proved this and here's what it looks like in English, but here's what the statement of the theorem”

“looks like in a formal language." And then the proof is one hundred pages long. Uh, and, and translating the proof into this language would be a, you know, would, would be like a PhD thesis worth of work, you know, a gigantic problem.”