Warning: Slop! Maybe WIP.
This repo is an experiment in consolidating and distilling many sources to arrive at a single source for assist LLMs in doing math with Lean and optionally mathlib. If I continue with this stuff, it'll hopefully get less sloppy. However, this sort of content seems to be controversial.
Everything here was initially generated by Claude Opus 4.6 Extended via the
Claude web app and then further developed by Codex using GPT 5.4 xhigh.
If you like to live dangerously, you might want to have your agent
clone this repo and then use it as it sees fit. Then contemplate.
The entry-point skill document is Skill Overview. The
detailed mathematical reference begins with
skills/ROOT.md.
Currently tools are fair game here. We won't emphasize MCP and instead prefer CLI tools.
Scary: clawresearch is a workspace for a claw-like
agent looking for material for this repo.