10 tagged lean, measured the same way as everything else here.
Browse within: quantconnect 5quantitative-finance 5
afhverjuekki/claude-code-aristotle-plugin
Skill Claude CodeCodex
This skill should be used when the user asks to "prove a theorem", "formalize to Lean", "use Aristotle", "fill sorries", "verify proofs", "verify algorithm", "verify code correctness", "check implementation", "find bugs in code", "work with Lean 4", "VERINA", or needs guidance on theorem proving, code verification…
Skill Claude CodeCodex
Build, smoke-test, publish, and verify the Q-agent Docker image (LEAN CLI + infrastructure pipelines + marimo). Handles LEANVERSION bumps, local iteration, GHCR pull verification, and CI debugging for the docker workflow.
Skill Claude CodeCodex
Push a QuantConnect project to QuantConnect Cloud via lean cloud push. Use when the user wants to deploy a LEAN algorithm to the cloud.
Skill Claude CodeCodex
Run a local QuantConnect research notebook in the correct LEAN Docker environment, inspect executed outputs, extract rendered charts, and interpret the results. Use when the user asks to run, debug, validate, or explain a notebook under MyProjects//research/.ipynb.
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…
Skill Claude CodeCodex
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…
Skill Claude CodeCodex
Find out what a Lean 4 project actually rests on, and why. Reports every theorem reaching a sorry anywhere upstream, everything settled by nativedecide rather than the kernel, and the shortest path from any declaration to any axiom with each hop labelled a statement dependency or a proof dependency. Use when the user…
Skill Claude CodeCodex
Check whether a machine-generated Lean 4 proof actually proves its theorem. A proof can appear in the environment, pass lake build, and still not have been proved: when elaboration fails Lean admits the declaration carrying sorryAx, which an axiom report cannot tell apart from a sorry somebody typed. Use when auditing…