Withdrawn

PLAN.md

@@ -46,8 +46,9 @@ The repo currently ships 235 problems, including the 50 AnnalsChallenge
 statements that landed in
 [lean-eval#532 feat: add 50 AnnalsChallenge problems](https://github.com/leanprover/lean-eval/pull/532).
 Submissions arrive as GitHub issues on lean-eval-submissions, are evaluated by
-comparator (with nanoda as an independent kernel) in GitHub Actions, and land as
-sticky `(user, model, problem)` records in the append-only results store. The
+comparator in GitHub Actions, and land as sticky `(user, model, problem)`
+records in the append-only results store. Nanoda remains integrated as an
+independent kernel but is temporarily disabled for submission performance. The
 leaderboard regenerates from that store daily.
 
 The system works, but it's showing strain:
@@ -400,8 +401,8 @@ in this document's history and can be revived.
 
 ## 6. Independent kernel validation
 
-After the recent soundness discoveries, this is a priority: as well as the
-standard kernel and nanoda, test submissions against a selection of the
+After the recent soundness discoveries, this is a priority: alongside the
+standard kernel, evaluate nanoda and a selection of the
 experimental kernels at the
 [Lean Kernel Arena](https://arena.lean-lang.org), collecting both acceptance
 and performance data. A checker is eligible for **required validation** when it
@@ -422,15 +423,14 @@ incorrect acceptance or rejection.
   10x to 40x faster than official on the Mathlib export) each fail exactly one
   soundness test (`extra-rec`). Each is one fix away from candidacy, and we
   should tell their authors so.
-- `nanoda`, which we already require, has zero incorrect results but declines
-  nine tests. Note also that the arena pins a different nanoda fork and
+- `nanoda`, which is integrated but temporarily disabled, has zero incorrect
+  results but declines nine tests. Note also that the arena pins a different nanoda fork and
   revision than we do; the pins should be reconciled.
 
 **Plan.**
 
 - **Close known holes first.** Before the broader replay, check each known
-  stable-kernel failure against the current official-plus-nanoda required
-  checks. If a
+  stable-kernel failure against the official checker and a nanoda replay. If a
   known exploit passes both, update the required pin or temporarily reject the
   affected construct before accepting more submissions.
 - **Backtest immediately.** I'll decrypt the audit archive; the replay queue

README.md

@@ -204,11 +204,12 @@ that tells comparator to check your theorem from the `Submission` namespace.
 lake test
 ```
 
-`lake test` shells out to four external tools that you must install yourself:
-`landrun` (the sandbox), `lean4export` (exports oleans to text), `comparator`
-(the verifier), and `nanoda` (the independent kernel). `WorkspaceTest` forces
-comparator to replay every Solution through nanoda, so a missing `nanoda_bin`
-fails the check. All four are pinned to immutable commits; the authoritative
+`lake test` shells out to three required external tools that you must install
+yourself: `landrun` (the sandbox), `lean4export` (exports oleans to text), and
+`comparator` (the verifier). Nanoda remains integrated as an independent kernel,
+but `WorkspaceTest` temporarily disables it for submission performance, so
+`nanoda_bin` is not currently required. All four tools are pinned to immutable
+commits; the authoritative
 pin table lives in [`SECURITY.md`](SECURITY.md) ("Trusted dependencies and pin
 policy"), and CI installs exactly these in
 [`.github/workflows/ci.yml`](.github/workflows/ci.yml). Reproduce that setup
@@ -236,10 +237,9 @@ git clone https://github.com/leanprover/comparator.git
   lake build comparator )
 export PATH="$PWD/comparator/.lake/build/bin:$PATH"
 
-# nanoda — the external kernel. WorkspaceTest forces comparator to replay the
-# Solution through nanoda, so `lake test` fails unless `nanoda_bin` is on your
-# PATH. Needs a Rust toolchain (`cargo`); the pin is on the source commit, not
-# the compiler version.
+# nanoda — the external kernel. It is temporarily disabled by WorkspaceTest;
+# install it when testing or restoring independent-kernel replay. Needs a Rust
+# toolchain (`cargo`); the pin is on the source commit, not the compiler version.
 git clone https://github.com/robsimmons/nanoda_lib.git
 ( cd nanoda_lib
   git checkout 68d5ca9db226849b41a6fff59d796ff19d0a8840

SECURITY.md

@@ -347,26 +347,19 @@ escaping, the triage gate) are in the submissions repo's `SECURITY.md`.
    sufficiently constrain a def — and adding one would be at most a
    heuristic. The real guard is PR review of any problem that uses
    def/instance holes.
-5. **Dual-kernel defence.** nanoda is a global requirement, not a
-   per-problem option. `templates/WorkspaceTest.lean` (the harness that
-   invokes comparator, propagated verbatim into every workspace and
-   rebuilt from the template by `run-eval`) reads the committed
-   `config.json`, overrides `enable_nanoda := true`, and hands that to
-   comparator — so nanoda runs regardless of what any config file says.
-   This mirrors comparator-live, which forces the flag at the invocation
-   site (`exec.ts`) and leaves project configs untouched. A single Lean
-   kernel soundness bug (e.g. the Lean-conjecture counterexample) no
-   longer suffices to claim false credit; the proof must be accepted by
-   both kernels. The residual risk narrows to a bug present in *both*
-   kernels, or in comparator's export/axiom comparison itself. Note the
-   pinned nanoda is `robsimmons/nanoda_lib` (the fork comparator-live
-   deploys); the `builtinTargets` widening in comparator's `Main.lean`
-   still carries a `TODO: fix when nanoda fixes its string handling`, so a
-   nanoda string soundness gap would not be caught. Because enforcement
-   lives in `WorkspaceTest`, a workspace whose committed `config.json`
-   still says `enable_nanoda: false` is not a bypass — the harness
-   overrides it. Bumping the nanoda pin follows the "Bumping pinned
-   dependencies" procedure above.
+5. **Dual-kernel defence (temporarily disabled).** Nanoda remains integrated
+   and pinned, but `templates/WorkspaceTest.lean` currently overrides
+   `enable_nanoda := false` globally for submission performance. Production
+   acceptance therefore relies on comparator's export/axiom checks and Lean's
+   default kernel; it does not currently receive an independent-kernel replay,
+   so a Lean kernel soundness bug is not independently checked by nanoda. Flip
+   the template's boolean back to `true` to restore the dual-kernel policy for
+   every regenerated workspace. The pinned nanoda is
+   `robsimmons/nanoda_lib` (the fork comparator-live deploys); the
+   `builtinTargets` widening in comparator's `Main.lean` still carries a
+   `TODO: fix when nanoda fixes its string handling`, so a nanoda string
+   soundness gap would not be caught after re-enablement. Bumping the nanoda pin
+   follows the "Bumping pinned dependencies" procedure above.
 
 ## References
 

templates/WorkspaceTest.lean

@@ -2,21 +2,19 @@ import Lean
 
 open Lean
 
-/-- Invoke comparator on this workspace, forcing the external nanoda kernel on.
+/-- Invoke comparator on this workspace with the external nanoda kernel disabled.
 
-nanoda is a global requirement of the eval, not a per-problem option: every
-solution must be accepted by comparator **and** replayed through nanoda's
-independent kernel. Rather than encode that in each workspace's `config.json`,
-this harness reads the committed config, overrides `enable_nanoda := true`, and
-hands the result to comparator — so nanoda runs regardless of what the file on
-disk says. This mirrors the comparator-live "gold standard" setup, which forces
-nanoda at the invocation site and leaves project configs untouched. -/
+Nanoda remains integrated and pinned, but is temporarily disabled globally for
+submission performance. This harness overrides `enable_nanoda := false` rather
+than relying on each workspace's committed `config.json`. Comparator still
+checks the exports and replays the solution through Lean's default kernel. Flip
+the boolean below back to `true` to restore independent-kernel replay. -/
 def main : IO UInt32 := do
   let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator"
   try
     let configText ← IO.FS.readFile "config.json"
     let config ← IO.ofExcept (Json.parse configText)
-    let config := config.setObjVal! "enable_nanoda" (Json.bool true)
+    let config := config.setObjVal! "enable_nanoda" (Json.bool false)
     IO.FS.withTempFile fun handle enforcedPath => do
       handle.putStr config.pretty
       handle.flush
@@ -27,7 +25,7 @@ def main : IO UInt32 := do
       child.wait
   catch err =>
     IO.eprintln s!"Failed to run comparator via `{comparatorBin}`."
-    IO.eprintln "Make sure `comparator` and the `nanoda_bin` external kernel are installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
-    IO.eprintln "See the root repository README for comparator setup details, including landrun, lean4export, and nanoda."
+    IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`."
+    IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export. `nanoda_bin` is additionally required when nanoda is enabled."
     IO.eprintln s!"Original error: {err}"
     pure 1