My personal belief is that translating an informal proof from a paper to a proof in Lean, given that the prerequisites are already formalized, is an O(n) operat

My personal belief is that translating an informal proof from a paper to a proof in Lean, given that the prerequisites are already formalized, is an O(n) operation where n is the length of the proof. It's just translation. Right now the constant is something like 10-100, but I think with more work on matlib and AI assistance it can be brought down to maybe 1-3, meaning formalising proofs right as you write them becomes feasible. In fact the constant may go below 1 as formalization in Lean can prevent unseen errors from slowing your progress.