fix(proof-synthesis): correct two miscited arXiv claims - #130
Merged
Conversation
… sweep) Verified every external citation in the skill against the actual sources (WebFetch of each arXiv page). Findings: - arXiv 2605.26457 (Verus-SpecGym, '26% LLM-as-judge miss'): CORRECT — a prior honesty pass wrongly flagged it as future-dated/unconfirmed; the paper is real (May 2026, Parno/Welleck et al.) and states the figure verbatim. No change. - arXiv 2409.13082 (AutoVerus, 90%/150 tasks): CORRECT. - arXiv 2511.17330 (AutoRocq): CORRECT. - miniF2F '100%': CORRECT (Seed-Prover 100% valid / 99.6% test, 2507.23726). Two fixes: - arXiv 2511.11829 was MISCITED for the Lean row — it is about NL-requirement autoformalization, not Lean-4 spec-equivalence proving. Re-pointed to CLEVER (2505.13938), which actually does prove Lean spec-equivalence. - Softened the CLEVER claim: 'no SOTA agent verifies more than 1 / spec-equivalence the dominant wall' is not supported by the source's abstract; reworded to the supported 'struggle to achieve full verification; the spec is the first-class hard task.' Version: skill 0.4.0 -> 0.4.1; plugin 0.14.0 -> 0.14.1. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
A claim-verification sweep of every external citation in the proof-synthesis skill (each arXiv page fetched and checked against the claim it backs).
Verified correct (no change): 2605.26457 (Verus-SpecGym '26% miss' — real, states the figure verbatim; a prior no-web honesty pass had wrongly flagged it), 2409.13082 (AutoVerus 90%/150), 2511.17330 (AutoRocq), miniF2F 100% (Seed-Prover).
Fixed:
Version: skill 0.4.0 → 0.4.1; plugin 0.14.0 → 0.14.1.
🤖 Generated with Claude Code