substitute axle check to diagnostic with server

[caosip]

• Switched to using the LEAN4_SERVER_URL env parameter to specify the server URL.
• Haven't tested if the Lean diagnostic tool still works yet.
• Replaced all instances of axle check with diagnostic in the prompts and skills.
• Folders in skills (excluding cli and SKILL.md) can be copied directly to .claude/skills/, and Claude will automatically recognize these skills.

[caosip]

• Now we use lake env lean targetfile.lean to replace the lean server. This solution enables local parallel checking and calls the import for local lean file. The only difference is that after adding the local lean file, lake build required (which has been mentioned in the prompt). The CLI implementation is in lean_check.py.
• An evaluation mode prompt has been added, and descriptions related to "only working on one sorry" have been removed.
• The only thing to note is that the checking solution may have CPU bottlenecks, so try to avoid having more than 10 tasks running in parallel.