Recent work - https://arxiv.org/pdf/2601.03768 - https://arxiv.org/pdf/2602.20082 (idea: running multiple agents to solve proof goals in parallel)
- Tips:
- Which model: Use the best model
- it is always more money-saving to get your code right at the first time
- Which Agent/CLI:
- Not OpenClaw: waste of tokens and risk of hallucination
- Use MCP:
- Rocq: vsrocq PR #1194 todo check if this is the one I am using
- Lean: lean4-mcp
- Which model: Use the best model
- Caveats:
- Agent can cheat:
- false admits
- silent definitions changes
- original lemma changed
- Put hard rules in
AGENTS.md,CLAUDE.md
- Agent can cheat:
- Setup Remote Access to a persistent running agent
- todo Git Worktree to Run Multiple Agents on the same project (check OpenAI’s official Codex documentation)
- Use voice inputs: Use typeless or similar voice to text tools.