I need a version of this for Lean 4; perhaps I can adapt this code.

AI generally struggles with less popular languages, and particularly with Lean 4, which is an excellent general purpose programming language that happens to have a primary goal to be a proof assistant. This skew in the training corpus really confuses AI.

Claude Opus 4 does better. I've looked at ways to serve the Lean 4 documentation; this Zig project is a better model for me.

Nia (https://www.trynia.ai) should generalize these tools, but it appears to have a "code base" focus for now. The right approach, but too specific a "system prompt".