Why wouldn't you just use coding agents and ensure you have e.g. Lean and Mathlib in the environment?

Also curious about this, it seems like it would be important to guide these tools more specifically based on the domain of expertise.