What's the best way to go from math paper => formalised Lean proof that is reliable these days?

Are specialist harnesses even needed?