Why wouldn't you just use coding agents and ensure you have e.g. Lean and Mathlib in the environment?
the system prompt could be narrower, for instance. there's no reason for such a harness to know about React stuff, for instance.
the system prompt could be narrower, for instance. there's no reason for such a harness to know about React stuff, for instance.