Evidence about LMLExplore

Reviews, problem reports, questions and tests of the declarations of LMLExplore, kept in evidence/ as S3 records: one per line, in git, never edited. They are written from the issues of this repository.

Adding to it

Open an issue with one of the forms: review a declaration, report a problem, ask a question, propose a test, list a test, or name a result. A bot turns it into a record, keyed by the declaration's hashes at the commit of LMLExplore you name (the latest if none), and replies on the issue. A record says which version of the declaration it was about: when the declaration, or something it rests on, changes, pages show the record as made on an earlier version.

Comments on the issue are replies. Commands in a comment change a record's state: /withdraw, /fixed <commit>, /intended, /invalid, /answered, /met <declaration>, /reopen. Records are never anonymous: each names the GitHub account it came from, and an AI agent's are labelled as such. An agent can also submit from a terminal with evidence-store submit.

Where the records show

• LMLExplore's site, built by LMLExplore's CI with referee-site, shows them on each declaration as of its latest build.
• This store imports the LeanMachineLearning store and the Mathlib probability store, so the site also shows reviews of the LML and Mathlib declarations LMLExplore rests on, marked with their store. A review of an LML declaration belongs in the LeanMachineLearning store, where LML's own site shows it too.

How it is set up

• evidence/store.json: the store's name (LMLExplore), the library, where its datasets are (the releases dataset-<commit12> of LMLExplore, which its CI publishes), and the stores it imports.
• .github/workflows/evidence-intake.yml and evidence-check.yml: intake, and the check of every change to the store, by evidence-store v0.7.2. They and the issue forms are those of the LeanMachineLearning store.