Spaces:

DineshAI
/

nPC7M7XLEv

Running

App Files Files Community

nPC7M7XLEv / README.md

DineshAI

Add Lean kernel verification for Claims 1 2 and 6

819b602 verified 2 days ago

preview code

Raw

History Blame Contribute Delete

852 Bytes

metadata

title: Convex Distance Operator Transport (nPC7M7XLEv)
emoji: 🎯
colorFrom: yellow
colorTo: red
sdk: static
pinned: false
tags:
  - trackio
  - trackio-logbook
  - open-experiment
  - icml2026-repro
  - paper-nPC7M7XLEv

CDOT reproduction — Lean kernel verification added

The previous live score is 9/12 at revision e7c9bd313c5bc8f5d252f0f5ac2dce3e087ba032. This additive candidate addresses the only remaining deductions—Claims 1, 2, and 6—with pinned Lean 4.19.0/mathlib kernel checks, an independent replay, and a false-theorem negative control. It is a forecasted improvement, not a new judge score.

Open the logbook at CURRENT — CDOT kernel-checked claim reproduction. Every file from the 9/12 revision remains preserved; the rejected human-only theoretical pages are reachable under Historical rejected baseline.