Add the conjectures contribution toolkit: review, proof verification, evidence and evaluations - #5386
Draft
williamjblair wants to merge 86 commits into
Draft
williamjblair wants to merge 86 commits into
williamjblair wants to merge 86 commits into
Conversation
A second-pass semantic review for Formal Conjectures pull requests. It answers one question, whether the Lean statement says what its cited source says, and leaves style, naming and imports to CI and AGENTS.md. The default path is one pass: bind the scope, run the focused build, read the cited source, compare meanings, report or stop. Escalation has named triggers, so the expensive work (whole-document reads, cross-references, Lean witnesses, history) runs when something calls for it rather than on every file. Findings carry a witness, what that witness shows and does not show, and the smallest proposed change. The output is publishable to GitHub as-is, and the review is advisory: it does not approve, merge, label, or touch a contributor branch. evals/evals.json records the measurement history, including a three-arm run against no skill and against an earlier version of this skill, over eight cases built by reverting merged fixes onto main. This skill matches the unaided reviewer's cost and wall clock, catches a case the unaided reviewer misses, and files a quarter as many items. The false-positive control returns CLEAN with no findings, where both other arms file nits. That run also records the measure the earlier iterations lacked. A suite where every case has a planted defect rewards recall and charges nothing for a finding that should not have been filed, so the file now reports findings filed alongside pass rate.
The monolithic defect-classes reference becomes four rubric files - _common, source-fidelity, statement-soundness, metadata-hygiene - the shape TauCetiProject/TauCetiReview uses, so a finding names the kind of defect it is, coverage is checkable per angle, and the rubrics could be judged independently by a runner without rewriting them. SKILL.md's compare step routes through the angles; the fast path is otherwise unchanged. The restructure initially regressed exactly the verification behaviours the assertion hardening of iterations 9-11 exists to detect, and the eval loop caught and repaired it: witnesses are checked rather than argued, escalation is mandatory for any verdict-setting finding, a source construction runs as a positive control when faithfulness rests on it, and a formal_proof root link stays a finding even after private resolution. Post-fix runs restore the ceiling on both active cases, 9/9 on 940 and 8/8 on ClaudesCycles, with each rule attributable to the single assertion it flipped. iteration_16 records the loop.
…o codex/fc-toolkit-cli
github-actions
Bot
added
the
documentation
williamjblair
changed the title
This was referenced Sep 11, 2026
…ration branch The CLI, review preparation, proof workspaces, evidence publishing and Harbor evaluation now ship together. Former google-deepmind#5387 is consolidated here; the website evidence display remains in google-deepmind#5388.
williamjblair
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
One
conjecturescommand for contribution work on FC: browse exact statements, prepare a review for a contributor's existing agent, verify a proof against an exact declaration, archive evidence and export frozen proof tasks for agent evaluations. This PR is the complete toolkit. It absorbs the former #5356 and #5387.Draft. Depends on #4899, #5375 and #5337. The diff against
mainincludes those three PRs until they merge. Changes beyond the prerequisites are thetoolkit/package, packaging and toolkit workflows. The review scripts from #4899 and the exporter from #5337 now delegate their shared logic totoolkit/.doctor,find,showreview --pr N/--changed, thenreview finish RUNinit TARGET --out DIR,verify DIRevidence publish RUNeval export SUITE,eval summarize/reviewworkflowAgents own model selection and authentication. Runs stay local by default. Actions preparation, publication and remote verification require explicit maintainer configuration; this PR enables none of them.
Qualification on the fork
mainon 16 September: every upstream check passed atb9f835b9, including the full Lean build, package export and macOS/Linux packaging. On the integration branch built from the same content, Harbor qualification returned all four expected outcomes again and Linux proof controls passed all eight cases.Pins. Tool pins still name the fork revisions of leanprover/lean-eval-generator#7 and leanprover/comparator#87. Both are open for review; affected checks rerun after adopting accepted revisions.
Website evidence display is #5388. Roadmap and merge order: #4394. Acceptance: #5376.