learnings: Voyager operating patterns from 2026-08-08

[CBirkbeck]

Community Teaching Contribution

Three user_teaching entries recorded while operating the Voyager daily update on the Lean Zulip, added as data/community_learnings/20260808_85b75bef.jsonl.

Entries

voyager, curation, announcement_policy — Curate, don't enumerate. Passing the novelty, significance and dedupe gates earns a result eligibility, not a bullet; keep the list short and interesting rather than exhaustive, and never pad a message to look productive. A long list is evidence of under-curation, and omitting a real result costs nothing, because the permanent dedupe keys on cited PR numbers. (Owner decision, after an update ran to thirteen bullets. Superseded in part on 2026-08-09 — see the update below: no length target in either direction.)

voyager, watermark, git_sha, data_integrity — Never pad or retype a git SHA into the state DM. Copy the full hash exactly as git rev-parse origin/docgen prints it, and verify with git cat-file -t <sha> before sending. A plausible 40-character string that names no object makes the next run's window unresolvable, and nothing downstream notices. If a bad one escapes, send a superseding DM — the protocol reads the newest.

voyager, significance_gate, prompt_framing, unproved_endpoint — Describe candidates to the ChatGPT significance gate in the words of the file's own ## Main results, not in the words of the roadmap milestone they serve. The gate can only judge the summary it is given, so an overstated summary returns ANNOUNCE for something unproved: a batch of adic-spaces PRs described as "establishing that the valuation spectrum is a spectral space" earned that recommendation while no SpectralSpace conclusion existed anywhere in the tree. Find the theorem statement, or do not announce it.

Update 2026-08-11 — corrections from the 2026-08-09..10 runs

Three further user_teaching entries, added as data/community_learnings/20260811_1d857014.jsonl:

voyager, curation, no_target_length — Sharpening that supersedes the "keep the list short" framing above: there is no minimum and no maximum bullet count — interest is the only test. Never pad a thin window, and never drop an interesting result to hit a number (a five-bullet message once cut the Huber/Tate Layer-0 block purely for the count). One bullet or ten are both correct if that is what the window held.

voyager, candidate_extraction, read_pr_bodies — Read the contents/body of every merged PR in the window, all prefixes; titles order the reading, never exclude a PR. Title-tone triage caused the worst miss so far: fifteen feat(EllipticCurve) PRs across two windows, none opened, zero elliptic-curve results in 105 announced bullets (TauCeti#2248, #2254, #2268 among the casualties).

voyager, significance_gate, interest_ranking — The batched ChatGPT gate runs on every pass, previews included, and doubles as the second opinion on how interesting/noteworthy each result is; its ranking, not discovery order, drives bullet order. Verdicts remain advice, not authority.

Note for the maintainer

The same lessons are also written as prose into skills/voyager/SKILL.md and HANDOVER.md on branch voyager/curate-not-enumerate (five commits ahead of main, PR open). These files are the machine-readable record; the branch is the operating documentation. Merging both is fine — they don't overlap textually — but the branch is the one that changes bot behaviour.

---

Auto-contributed by mathlib-quality /teach command.