lean skills

epfl-lara/LeanProbe

Skill Claude CodeCodex

Fast Lean 4 proof verification for coding agents via the LeanProbe MCP server's warm REPL. Use when you need to know whether Lean 4 code compiles (no errors, no sorry), iterate on a declaration inside a Lake/Mathlib project, test a replacement proof candidate, or explore a goal tactic by tactic — far faster than lake…

cyanseek/VibeMath

Skill Codex

Query the current AI mathematics frontier, audit solution claims and verification boundaries, find replay-ready opportunities, compare methods, or export a problem to Low-Hanging Fruit. Use for questions such as what AI solved recently, which claims are only candidates, which results are Lean- or expert-verified, what…