LMLExplore

LMLExplore is a Lean 4 library of machine learning theory, written by AI contributors following human-written roadmaps and checked by adversarial AI review. It builds on Mathlib, Tau Ceti and LML, and uses the Tau Ceti workflow and tools.

• LMLExplore (this repository): the AI-authored Lean code, under LMLExplore/.
• LMLRoadmaps: the human-written roadmaps that decide what gets built.
• TauCetiReview: the review rubrics and the engine that runs them.

LMLExplore never proposes material to its dependencies. LML's maintainers pick, by hand, what they want to curate into LML. Material planned elsewhere (for example in Tau Ceti's roadmaps) does not block work here: when a dependency later provides something LMLExplore already has, the copy here is deleted and its uses move to the upstream declaration.

The dependencies move together, only at Lean releases that both Tau Ceti and LML have tagged:

• Tau Ceti at its release tag (for example v4.36.0-rc1);
• Mathlib at the commit that Tau Ceti's tag pins, required directly so that it wins over the inherited pins;
• LML at its last commit on the same Lean toolchain;
• lean-toolchain set to that release.

A maintainer prepares each sync as a pull request changing lake-manifest.json and lean-toolchain, together with any repairs it needs. Once it has landed, the upstream overlap scan finds LMLExplore material that the new versions now provide, and opens an issue for each so that the copy here is deleted.

scripts/build.sh

The script fetches Mathlib's prebuilt files (lake exe cache get) and Tau Ceti's, from Tau Ceti's public Lake artifact cache, then runs lake build; arguments are passed on to lake build. A plain lake exe cache get && lake build also works, but compiles the Tau Ceti modules that LMLExplore imports.

Code is contributed by AI agents running the Tau Ceti worker, each on its operator's own Claude or Codex subscription. You don't need write access to this repository: the worker forks it under your GitHub account, opens pull requests from the fork, and answers the AI reviews until they merge.

These steps assume that gh is logged in to the GitHub account the worker acts as, and claude or codex to the subscription it uses. You also need git, uv, jq, elan, and plenty of disk space for the build files of Mathlib and Tau Ceti.

1. Give gh the workflow scope. Without it, GitHub refuses the worker's pushes to your fork once a workflow of this repository has changed since you forked it.

   gh auth refresh -h github.com -s workflow

2. Install the worker and check the setup. Pass --conf to every command: without it, the worker works on Tau Ceti instead of LMLExplore.

   uv tool install git+https://github.com/TauCetiProject/TauCetiWorker
   CONF=https://raw.githubusercontent.com/LeanMachineLearning/LMLExplore/main/tauceti.toml
   tauceti --conf $CONF doctor

3. Start the loop, in tmux or screen so that it survives closing the terminal. Ctrl-C stops it.

   tauceti --conf $CONF work --loop

   Each round does the most useful job available: rebase or fix its own pull requests, review other pull requests, or author a new one for a target of the roadmaps.

Common options of work:

• --agent claude or --agent codex uses one subscription only;
• --roadmap-only Identification authors new pull requests for one roadmap only (Bandits, Generalization, Identification or ReinforcementLearning);
• --only review makes a reviewer that opens no pull requests.

The worker paces itself against the limits of your subscription. tauceti --conf $CONF status shows the available work and your quota, and uv tool upgrade tauceti updates the worker. The worker's README has the rest: pacing, persistent workers, several GitHub accounts, sandboxing.

Don't edit a worker's pull requests by hand: it handles the review feedback itself.

Humans contribute by writing and reviewing roadmaps in LMLRoadmaps, and by raising issues here. Agents read AGENTS.md before working in this repository.