feat: DeterministicScore proofs + ITP 2026 paper package#2
Merged
Conversation
Lean 4 (Score/DeterministicScore.lean): - 51 theorems, zero sorry, verified with Lean 4.25.2 + Mathlib v4.25.2 - Total order, RuntimeValid invariant, saturating arithmetic branch specs - Abstract float conversion model, scalar mul/div, MIN-unreachability Paper package (papers/2026-deterministic-score/): - LIPIcs/ITP 2026 format, main.tex with correspondence table - claims.yaml, correspondence.yaml, proof-map.yaml - Validation scripts for scope and forbidden overclaims - Artifact description referencing khive-score (canonical) and ruvector (port) Tooling: - .pre-commit-config.yaml: markdownlint, sorry check, lake build, LaTeX scope - .gitignore: exclude .lake/, LaTeX build artifacts Co-Authored-By: claude-flow <ruv@ruv.net>
- Lean build: elan install, Mathlib cache (keyed on toolchain+manifest), lake build, sorry check, theorem count gate (≥51) - Paper validation: claims registry, forbidden phrases, scope audit - Markdown lint via markdownlint-cli2-action Co-Authored-By: claude-flow <ruv@ruv.net>
- Convert hard tabs to spaces in STANDARDS.md - Add blank line after heading in README.md Co-Authored-By: claude-flow <ruv@ruv.net>
CC BY 4.0 is the standard license for academic proof artifacts and aligns with LIPIcs/Dagstuhl publishing requirements. Co-Authored-By: claude-flow <ruv@ruv.net>
The grep was scanning Mathlib dependencies in .lake/packages/, which contain sorry in test files (plausible tactic tests). Co-Authored-By: claude-flow <ruv@ruv.net>
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.
Summary
sorry, cleanlake buildwith Lean 4.25.2 + Mathlib v4.25.2.gitignorefor Lean/LaTeX build artifactsArtifact references
github.com/ohdearquant/khive—crates/khive-scoregithub.com/ohdearquant/RuVector—feat/deterministic-scoringbranch (PR ITP 2026 submission checklist — DeterministicScore #1)Test plan
lake build— 51 theorems verified, 0 errors, 0 warningsgrep sorry— 0 resultscheck_claims.py— 10 claim IDs, all classes presentcheck_no_forbidden_claims.py— no overclaimscheck_scope.sh— scope audit passed🤖 Generated with claude-flow