ok this [CLAUDE.md](π.md ) actually made a huge difference (at least for Opus), it is now working methodically and actually is closing in on the correct proof. previously it was working in big unthinking swipes and was getting completely lost
RE:
what's the latest on connecting Claude Code to LSP? ideally i'd want it to pick up whatever my VS Code is using. is that possible? (concretely, i'd like to it to connect to my Lean LSP)
okay the "show less" bug is fixed but i'm just getting `nettop` now. i think it would be good if "show less" was honored for `nettop` too, even if Discover has nothing to show at all. i'd rather take nothing over `nettop`