feat(lean): import 47 Lean 4 theorems — machine-checked auction core#1
Merged
Conversation
Adds machine-checked formal verification of the Nexbid auction core to the
protocol-commerce open-source repository. All 47 theorems are sorry-free
and pass `lake build` (verified locally 2026-05-15 in both source repo
and this destination).
Coverage:
- Score boundedness, KAN-consistency (Score, KanScore, Consistency, Normalize)
- Auction eligibility + winner selection (Auction, Monotone, EndToEnd)
- Atomic budget decrement safety (Budget — T7a-T7e + composition)
- Wallet payment bounds + idempotency (Wallet — W3/W5/W6a + L3)
- Commerce-layer revenue, policy, DSL (Commerce/{Revenue,Policy,DSL})
- Custom Rat-helper library (RatHelpers — closes Lean stdlib gaps without Mathlib)
NOT covered by these proofs (per README disclaimer): authentication,
RBAC, CORS, SSRF, network safety, TS-to-Lean implementation conformance.
Those are enforced by code review, tests, and red-team tests in the
private Nexbid main repository.
The `defaultRevenueShare` constant in Commerce/DSL.lean uses a generic
70/30 library default; theorems T8-T10 are generic over any
`share : RevenueShare` instance. Production Nexbid AdCP tier-pricing
(90/10 Standard, 95/5 Founding) is configured via
`packages/shared/src/pricing.ts` in the private operational repo and
per-customer overrides in `platform_pricing` (DB). README documents
this stratification explicitly.
CI: `.github/workflows/lean-build.yml` runs `lake build` plus a
sorry/admit grep-gate on every PR touching lean-verification/.
License: MIT — same as the rest of protocol-commerce.
Co-Authored-By: Claude Opus 4.7 (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.
Summary
Imports the Lean 4 formal verification suite from the private Nexbid main repository into this open-source protocol repo. All 47 theorems are machine-checked, sorry-free, and pass
lake build(verified locally 2026-05-15).This closes the audit-finding (
memory/lean-4-audit-2026-05-15.md) that the Lean-4 claim was real but unverifiable due to private repository. After merge, the claim "formally verified auction core" is publicly auditable for the first time.What is proven
0 ≤ score ≤ 1, bid-monotonicity, KAN within 2% of linear baselineWhat is NOT proven (disclaimer in README)
Authentication, RBAC, CORS, SSRF, network-safety, concurrency under real DB load, and TypeScript-to-Lean implementation conformance are NOT covered by these theorems. Those are enforced by code review, integration tests, and red-team tests (23 tests in the private Nexbid main repo).
Revenue-share library default (70/30 vs production 90/10)
The
defaultRevenueShareconstant inCommerce/DSL.leanuses a generic 70/30 library default. Theorems T8-T10 are generic over anyshare : RevenueShareinstance — the default is irrelevant for theorem applicability. Production Nexbid AdCP tier-pricing is 90/10 Standard / 95/5 Founding (configured viapackages/shared/src/pricing.tsin the private operational repo, with per-customer overrides in theplatform_pricingdatabase table).The README documents this stratification explicitly to avoid future drift-confusion.
CI
.github/workflows/lean-build.ymlruns on every PR touchinglean-verification/:--default-toolchain none.lake/directory keyed by lean-toolchain + lakefile + lake-manifest hashlake build(compiles + type-checks all 47 theorems)sorry/admitfound inNexbidVerify/Expected first-run duration: ~5-8 minutes (Lean toolchain download), subsequent runs ~30s (cached).
License
MIT — same as the rest of
protocol-commerce.Test plan
lake buildlocally in source repo (~/projects/nexbid/lean-verification): 17 jobs, 0 errorslake buildlocally in destination (this branch): 17 jobs, 0 errorsPost-merge follow-ups (separate work, private Nexbid repo)
website/src/pages/docs/VerificationDocsPage.tsx: "13 Theoreme" → 47 + link to public repoREADME.mdin private Nexbid repo: remove "Publikation Q2/Q3 2026"-caveat, link public repo🤖 Generated with Claude Code