I am curious if there is a “harness” for maths out there (like the system prompt and tool collection in Claude code but for maths instead of coding)?
Asking the llm to structure its response in plan and implementation, allowing it to call tools like python, sage, lean etc.
Also curious about this, it seems like it would be important to guide these tools more specifically based on the domain of expertise.
Why wouldn't you just use coding agents and ensure you have e.g. Lean and Mathlib in the environment?
I am not part of the scene but I am sure there is, Tao himself talks a lot about this type of thing