proximity-prize

KO | EN

gitlite — search

#containers #ai #open-source #awesome-list #github #c #computer-vision #command-line #python #shell

proximity-prize

(★ 9)

No description available.

File Explorer

ZIP Download

- - benchmark-irs-reduction-threshold-lower.yml
  - benchmark-irs-reduction-threshold-upper.yml
  - benchmark.yml
  - check-versions.yml
- comparator-leanchecker.patch
- comparator-upper.json
- comparator.json
- - IRSProfile.lean
  - TargetLower.lean
  - TargetUpper.lean
- - ActiveSliceAssembly6807.lean
  - ActualFirstCutPole6807.lean
  - ActualGenericChannel6807.lean
  - ActualSliceMultiplicity6807.lean
  - ActualWeightedFirstSlice6807.lean
  - AffineFactorAggregate6808.lean
  - BoundaryTailAlgebra.lean
  - BoundaryTailArithmetic.lean
  - BoundaryTailAsymmetric.lean
  - BoundaryTailBase.lean
  - BoundaryTailCoefficientFacts.lean
  - BoundaryTailComponent.lean
  - BoundaryTailCoordinate.lean
  - BoundaryTailCounting.lean
  - BoundaryTailDegrees.lean
  - BoundaryTailDualRetained6807.lean
  - BoundaryTailFixedStage.lean
  - BoundaryTailFlags.lean
  - BoundaryTailGates.lean
  - BoundaryTailGates6808.lean
  - BoundaryTailIdentity.lean
  - BoundaryTailIdentityArithmetic.lean
  - BoundaryTailInitial.lean
  - BoundaryTailInterpolation.lean
  - BoundaryTailJointBudget6807.lean
  - BoundaryTailKernels.lean
  - BoundaryTailLeadingCoefficient.lean
  - BoundaryTailNormalArithmetic.lean
  - BoundaryTailOrdinary.lean
  - BoundaryTailOrdinaryHigh.lean
  - BoundaryTailOrdinaryLow.lean
  - BoundaryTailOwnShape.lean
  - BoundaryTailPaddedIdentity.lean
  - BoundaryTailPole.lean
  - BoundaryTailProfile116.lean
  - BoundaryTailProfileCount.lean
  - BoundaryTailProjection.lean
  - BoundaryTailProvider.lean
  - BoundaryTailRealization.lean
  - BoundaryTailRecurrence.lean
  - BoundaryTailReduced.lean
  - BoundaryTailRefinedCap.lean
  - BoundaryTailRegularData.lean
  - BoundaryTailRegularGeometry.lean
  - BoundaryTailRepresentation.lean
  - BoundaryTailRetainedStage.lean
  - BoundaryTailRouting.lean
  - BoundaryTailSelection.lean
  - BoundaryTailSharpGate.lean
  - BoundaryTailTotalAvoidance.lean
  - BoundaryTailValuation.lean
  - BoundaryTailZeroCount.lean
  - CommonLinearChannels6807.lean
  - DualCutBridge6807Arithmetic.lean
  - FirstCutMultiplicityTransport6807.lean
  - FirstCutValuation6807.lean
  - FirstSlicePoleBudget6807.lean
  - GenericSlicePoints6807.lean
  - HigherAffineCheckedR016810.lean
  - HigherAffineCheckedR026810.lean
  - HigherAffineCheckedR036810.lean
  - HigherAffineCheckedR046810.lean
  - HigherAffineCheckedR056810.lean
  - HigherAffineCheckedR066810.lean
  - HigherAffineCheckedR076810.lean
  - HigherAffineCheckedR086810.lean
  - HigherAffineCheckedR096810.lean
  - HigherAffineCheckedR106810.lean
  - HigherAffineCheckedR116810.lean
  - HigherAffineCheckedR126810.lean
  - HigherAffineCheckedR136810.lean
  - HigherAffineCheckedR146810.lean
  - HigherAffineCheckedR156810.lean
  - HigherAffineCheckedR166810.lean
  - HigherAffineCheckedR176810.lean
  - HigherAffineCheckedR186810.lean
  - HigherAffineCheckedR196810.lean
  - HigherAffineCheckedR206810.lean
  - HigherAffineCheckedR216810.lean
  - HigherAffineCheckedR226810.lean
  - HigherAffineCheckedR236810.lean
  - HigherAffineCheckedR246810.lean
  - HigherAffineCheckedR256810.lean
  - HigherAffineCheckedR266810.lean
  - HigherAffineCheckedR276810.lean
  - HigherAffineCheckedR286810.lean
  - HigherAffineCheckedR296810.lean
  - HigherAffineCheckedR306810.lean
  - HigherAffineCheckedR316810.lean
  - HigherAffineCheckedR326810.lean
  - HigherAffineCheckedR336810.lean
  - HigherAffineCheckedR346810.lean
  - HigherAffineFiniteChecks6810.lean
  - HigherAffineRateBridge6810.lean
  - HigherAffineRateData6810.lean
  - HigherAffineSingleData6810.lean
  - HigherAffineSingleton6810.lean
  - HigherAssembly6810.lean
  - HigherBaseData6810.lean
  - HigherCertificate6810.lean
  - HigherClosure6810.lean
  - HigherCounting6810.lean
  - HigherCountingArithmetic6810.lean
  - HigherFiniteCertificate6810.lean
  - HigherIdentityArithmetic6810.lean
  - HigherInitial6810.lean
  - HigherInitialArithmetic6810.lean
  - HigherKernels80850.lean
  - HigherLedgerAudit6810.lean
  - HigherLedgerData6810.lean
  - HigherOrdinary6810.lean
  - HigherOrdinaryHigh6810.lean
  - HigherOrdinaryLow6810.lean
  - HigherPaddedIdentity6810.lean
  - HigherPairGeometry6810.lean
  - HigherPhaseCore6810.lean
  - HigherPhaseData6810.lean
  - HigherPhaseRuns6810.lean
  - HigherPhaseSemantics6810.lean
  - HigherProtocol6810.lean
  - HigherRegularBridge6810.lean
  - HigherRootArithmetic6810.lean
  - HigherRootAsymmetric6810P0.lean
  - HigherRootAsymmetric6810P1.lean
  - HigherRootAsymmetric6810P2.lean
  - HigherRootAsymmetric6810P3.lean
  - HigherRootCarrier6810P0.lean
  - HigherRootCarrier6810P1.lean
  - HigherRootCarrier6810P2.lean
  - HigherRootCarrier6810P3.lean
  - HigherRootFixedStage6810.lean
  - HigherRootIdentityBridge6810P0.lean
  - HigherRootIdentityBridge6810P1.lean
  - HigherRootIdentityBridge6810P2.lean
  - HigherRootIdentityBridge6810P3.lean
  - HigherRootInterpolation6810.lean
  - HigherRootLeadingCoefficient6810.lean
  - HigherRootOwnArithmetic6810P0.lean
  - HigherRootOwnArithmetic6810P1.lean
  - HigherRootOwnArithmetic6810P2.lean
  - HigherRootOwnArithmetic6810P3.lean
  - HigherRootOwnAssembly6810P0.lean
  - HigherRootOwnAssembly6810P1.lean
  - HigherRootOwnAssembly6810P2.lean
  - HigherRootOwnAssembly6810P3.lean
  - HigherRootOwnShape6810P0.lean
  - HigherRootOwnShape6810P1.lean
  - HigherRootOwnShape6810P2.lean
  - HigherRootOwnShape6810P3.lean
  - HigherRootProfileCount6810P0.lean
  - HigherRootProfileCount6810P1.lean
  - HigherRootProfileCount6810P2.lean
  - HigherRootProfileCount6810P3.lean
  - HigherRootRegularData6810P0.lean
  - HigherRootRegularData6810P1.lean
  - HigherRootRegularData6810P2.lean
  - HigherRootRegularData6810P3.lean
  - HigherRootRegularGeometry6810P0.lean
  - HigherRootRegularGeometry6810P1.lean
  - HigherRootRegularGeometry6810P2.lean
  - HigherRootRegularGeometry6810P3.lean
  - HigherRootSources6810.lean
  - HigherRootSourceStage6810P0.lean
  - HigherRootSourceStage6810P1.lean
  - HigherRootSourceStage6810P2.lean
  - HigherRootSourceStage6810P3.lean
  - HigherRootTotalAvoidance6810.lean
  - HigherRouting6810.lean
  - HigherScalar6810.lean
  - HigherSelection6810.lean
  - HigherShape6810.lean
  - HigherSingletonGeometry6810.lean
  - HigherSourceSound6810.lean
  - HigherTenPhase6810.lean
  - HigherThresholdClosed6810.lean
  - HigherThresholdData6810.lean
  - JointBudgetArithmetic6807.lean
  - LowerFoundation.lean
  - LowerGeometry.lean
  - PureFlagSliceBudget6807.lean
  - radius.txt
  - ReducedCommonLinear6807.lean
  - score.txt
  - SecondJetPointwiseBudgets6807.lean
  - SecondJetRefinements.lean
  - SmallSliceBudgets6807.lean
  - Solution.lean
  - ThreeChannelJoint6807.lean
  - WeightedPlaceOrder6807.lean
  - WeightedSliceAssignment6807.lean
  - WeightedZeroMass6807.lean
- - HalfRadiusCollision.lean
  - IRSHalfRadius.lean
  - OrbitPencil.lean
  - PrescribedTop.lean
  - score.txt
  - Solution.lean
  - unsafe-index.txt
- benchmark_contract.py
- cancel.py
- challenges.py
- check-axioms.lean
- check-submission-imports.sh
- check-versions.py
- explain-rejection.py
- render-benchmark-challenge.py
- submit.py
- verdict-gate.py
- write-benchmark-score.py
- write-verifier-score.py
- KernelEval.lean
- README.md
.gitattributes
.gitignore
AGENTS.md
benchmark.json
benchmark.sh
challenges.json
lake-manifest.json
lakefile.toml
lean-toolchain
LICENSE
ProximityPrize.lean
README.md
setup.sh

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

This repository defines two Lean challenges around the ABF26 reduction-error
threshold for one fixed interleaved Reed–Solomon profile. Each track includes
an editable baseline candidate.

Let

```text
epsilon* = 2^-128
q(delta) = (1 - delta)^128
b = B / 100
```

The score is the spot-check quantity induced by a certified threshold radius.
It is not `-log2(WSS)` and is not a full-protocol security claim.

## Challenges

The lower certificate is
`ProximityPrize.Benchmark.ProtocolClaim B P Q`. It uses ArkLib's certified
combination-round error for the executable IRS straight-line extractor. Since
ArkLib proves `winningSetDensity <= certifiedGammaError`, this is a
conservative safe point.

The upper certificate is
`ProximityPrize.Benchmark.Upper.ProtocolClaimUpper B i`. It certifies an entire
unsafe suffix because no monotonicity theorem for `winningSetDensity` is
assumed. The index is verified metadata; the leaderboard compares `B` only.

The protected definitions are in
[`TargetLower.lean`](ProximityPrize/Benchmark/TargetLower.lean) and
[`TargetUpper.lean`](ProximityPrize/Benchmark/TargetUpper.lean).

## Included baselines

These are editable starting points, not authoritative leaderboard results. The
lower baseline certifies the extractor-error target at radius `1/4`; the upper
baseline certifies that winning-set soundness exceeds the target throughout
the required half-radius suffix.

## Candidate layout

Lower submissions use:

```text
ProximityPrize/SubmissionLower/
  Solution.lean
  score.txt          # canonical non-negative centibits B
  radius.txt         # exact P/Q
```

and export:

```lean
theorem ProximityPrize.Benchmark.candidate :
    ProximityPrize.Benchmark.ProtocolClaim B P Q := by
  ...
```

Upper submissions use:

```text
ProximityPrize/SubmissionUpper/
  Solution.lean
  score.txt          # canonical non-negative centibits B
  unsafe-index.txt   # i, from 1 through 131072
```

and export:

```lean
theorem ProximityPrize.Benchmark.Upper.candidate :
    ProximityPrize.Benchmark.Upper.ProtocolClaimUpper B i := by
  ...
```

Each challenge stands alone: a candidate may import only its own protected
target and flat helper `.lean` files beside `Solution.lean` in the same
submission root. Cross-challenge imports and subdirectories are rejected. The
benchmark binds the scalar files to the exact theorem type and permits only
`propext`, `Classical.choice`, and `Quot.sound` in the candidate's axiom
closure.

## Run

Build the pinned verifier tools and protected targets:

```sh
./setup.sh
```

Then run the track whose submission root you created:

```sh
./benchmark.sh lower
./benchmark.sh upper
```

On a machine without the trusted Linux sandbox, an explicitly unranked smoke
test is available with `BENCHMARK_INSECURE_LOCAL=1`.

Yukon exposes both score directions from [`benchmark.json`](benchmark.json):

```sh
yukon switch irs-reduction-threshold-lower
yukon run

yukon switch irs-reduction-threshold-upper
yukon run
```

Local artifacts are diagnostic only. Ranked results require the independent
verifier to accept the exact commit and return the matching score plus exact
radius or unsafe index. The repository-side identities are:

```text
proximity-prize-reduction-lower @ irs-reduction-threshold-v10
proximity-prize-reduction-upper @ irs-reduction-threshold-v10
```

Those verifier profiles must be registered before either workflow can issue an
authoritative leaderboard score.

proximity-prize

File Explorer

# Use via CDN

Was this content helpful?

Recent Feedback

Download README