chore: bump to 2026-08-31 (#932)

Author: david-christiansen

.vale/styles/config/ignore/terms.txt

@@ -102,6 +102,7 @@ invalidField
 iterator
 iterator's
 iterators
+Landlock
 letterlike
 linearization
 linearize

Manual/Axioms.lean

@@ -181,7 +181,7 @@ Because they occur only in a proof, the compiler has no problem generating code:
 tag := "standard-axioms"
 %%%
 
-There are seven standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean:
+There are four standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean:
  * ```signature
    Classical.choice.{u} {α : Sort u} : Nonempty α → α
    ```
@@ -202,40 +202,11 @@ Uses of this axiom are not intended to occur in finished proofs, as it can be us
    sorryAx {α : Sort u} (synthetic := true) : α
    ```
 
-Three final axioms do not truly exist for their _mathematical_ content; from a mathematical perspective they prove trivial statements:
-
- * ```signature
-    Lean.trustCompiler : True
-   ```
-
- * ```signature
-    Lean.ofReduceBool (a b : Bool) : Lean.reduceBool a = b → a = b
-   ```
- * ```signature
-    Lean.ofReduceNat (a b : Nat) : Lean.reduceNat a = b → a = b
-   ```
-
-These axioms instead track proofs that depend on the correctness of the entire compiler, and not just on the much smaller {tech}`kernel`.
-
-:::example "Creating and Tracking Proofs That Trust the Compiler"
-The functions {name}`Lean.reduceBool` and {name}`Lean.reduceNat` can be invoked to have the compiler perform a calculation; this can greatly improve performance of implementations of proof by reflection.
-
-```lean
-def largeNumber : Nat := Lean.reduceNat (230_000 + 4_500 + 1_000_067)
-```
-
-The resulting term depends on the axiom {name}`Lean.trustCompiler` in order to track the fact that this calculation depends on the correctness of the compiler.
-
-```lean (name := printAxExC1)
-#print axioms largeNumber
-```
-```leanOutput printAxExC1
-'largeNumber' depends on axioms: [Lean.trustCompiler]
-```
-:::
+In addition to the standard axioms, proofs by native evaluation introduce a dedicated axiom for each computation that is asserted by the compiled code.
+These axioms track proofs that depend on the correctness of the entire compiler, and not just on the much smaller {tech}`kernel`.
 
 :::example "Axioms and the `native_decide` Tactic"
-Instead of appealing to {name}`Lean.trustCompiler`, the {tactic}`native_decide` tactic creates a bespoke axiom for each invocation.
+The {tactic}`native_decide` tactic creates a bespoke axiom for each invocation.
 This allows each axiom to be audited for the precise statement that it proves.
 
 ```lean (name := printAxExC2)

Manual/BasicTypes/BitVec.lean

@@ -166,8 +166,9 @@ tag := "BitVec-automation"
 %%%
 
 In addition to the full suite of automation and tools provided by Lean for every type, the {tactic}`bv_decide` tactic can solve many bitvector-related problems.
-This tactic invokes an external automated theorem prover (`cadical`) and reconstructs the proof that it provides in Lean's own logic.
-The resulting proofs rely only on the axiom {name}`Lean.ofReduceBool`; the external prover is not part of the trusted code base.
+This tactic invokes an external automated theorem prover (`cadical`) and validates the certificate returned by the prover with a checker that's written in Lean and proved sound.
+This verified checker is run as native code because reducing it in the kernel is not feasible for performance reasons.
+Because the kernel does not execute native code, the resulting proof relies on a dedicated axiom that asserts the outcome of the native computation; the external prover is not part of the trusted code base.
 
 :::example "Popcount"
 

Manual/BasicTypes/Float.lean

@@ -359,7 +359,7 @@ Floating-point numbers fall into one of three categories:
 ### Inequalities
 
 The decision procedures for inequalities are opaque constants in the logic.
-They can only be used via the {name}`Lean.ofReduceBool` axiom, e.g. via the {tactic}`native_decide` tactic.
+They can only be used via native evaluation, e.g. via the {tactic}`native_decide` tactic.
 
 {docstring Float.le}
 

Manual/BuildTools/Lake/CLI.lean

@@ -42,6 +42,7 @@ COMMANDS:
   check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   shake                 minimize imports in source files
+  challenge             judge a solution against a challenge
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
@@ -821,6 +822,176 @@ The {lakeMeta}`options` may be:
 
 ::::
 
+# Challenges and External Checkers
+%%%
+tag := "lake-challenge"
+%%%
+
+Lake supports invoking {ref "validating-comparator"}[`comparator`] to validate a proof against a challenge, including the use of external checkers.
+This should only be necessary in high-risk scenarios, such as proof marketplaces, high-reward competitions, or when dealing with potentially unaligned AI systems.
+
+```lakeHelp challenge
+Judge a solution against a challenge
+
+USAGE:
+  lake challenge --config <FILE>
+
+Establishes that every named theorem in the solution proves the same statement
+as the challenge, uses no axiom outside the permitted list, and is accepted by
+the kernel.
+
+The project is untrusted input: its configuration is evaluated, and its code
+built and exported, inside a `landrun` sandbox, and none of its `.olean` files
+is ever loaded into Lake's own address space. `landrun` is required; there is
+no unsandboxed mode, so this command is available on Linux only.
+
+The project has to carry a `lake-manifest.json`, because dependencies are
+resolved inside the sandbox and it cannot write to the project directory.
+Building the project once, before distributing it, is enough to write one.
+
+OPTIONS:
+  --config=<file>       JSON file describing the challenge (see below)
+
+CONFIGURATION:
+  The challenge author writes the file and distributes it with the project, so
+  that a solver need only point `lake challenge` at it:
+
+  {
+    "challenge_module": "Challenge",
+    "solution_module": "Solution",
+    "theorem_names": ["imo2024_p1"],
+    "definition_names": [],
+    "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+    "external_kernels": {"nanoda": ["nanoda_bin"]}
+  }
+
+  `challenge_module`, `solution_module`, `theorem_names` and
+  `permitted_axioms` are required; the rest may be omitted.
+  `definition_names` lists the challenge's definition holes.
+  `permitted_axioms` is deliberately not defaulted: it is what the verdict
+  means, so the challenge author states it. The three above are the ones
+  `#print axioms` treats as a clean proof.
+
+  `external_kernels` names additional checkers to run over the export, each as
+  the command to execute; the solution must satisfy every one of them as well
+  as Lean's own kernel. `enable_nanoda: true` is still accepted and is
+  equivalent to a "nanoda" entry of ["nanoda_bin"]; name the command in
+  `external_kernels` instead to run it from elsewhere.
+
+EXIT CODES:
+  0                     accepted
+  1                     rejected: statement mismatch, forbidden axiom, kernel
+                        rejection, or a build that did not succeed
+  2                     could not start: `landrun` or the manifest is missing,
+                        or the configuration is missing, unreadable or
+                        malformed
+
+ENVIRONMENT:
+  COMPARATOR_LANDRUN    sandbox executable (default: `landrun` on PATH)
+
+  The exporter is always the `leanexport` of this toolchain, and deliberately
+  not configurable: the export format has to match the compiler that produced
+  the `.olean` files being exported.
+
+HARDENING:
+  The sandbox bounds writes and TCP connections: only `.lake` is writable, and
+  only dependency resolution may connect, on the ports git's transports use.
+  It does not bound reads, execution, or non-TCP traffic.
+
+  Until the Landlock fix released in Linux 7.1 is widely available, `landrun`
+  can be escaped through an `AF_UNIX` socket. Where that matters, run the
+  command under a wrapper that removes the capability:
+
+    systemd-run --user --pty --property=RestrictAddressFamilies=~AF_UNIX \
+      lake challenge --config challenge.json
+```
+
+::::lake challenge "\"--config\" file"
+
+Judges a solution against a {deftech}_challenge_: a trusted configuration that states which theorems must be proved and which axioms are permitted.
+{lake}`challenge` establishes that every named theorem in the solution proves the same statement as the challenge, that the solution uses only permitted axioms, and that it is accepted by Lean's kernel as well as by every configured external kernel.
+
+The current Lake workspace is considered to be the {deftech}_solution_ project: it should satisfy the specification provided by the challenge.
+The solution is considered untrusted input.
+Its configuration is evaluated, and its code built and exported, inside a [`landrun`](https://github.com/Zouuup/landrun) sandbox, and its {tech}[`.olean` files] are kept out of Lake's own address space.
+Because `landrun` is required, the command is only available on Linux.
+The `landrun` executable name is determined by the {envVar +def}`COMPARATOR_LANDRUN` environment variable, defaulting to `landrun` if this is not set.
+The executable is resolved via the {envVar}`PATH`.
+The export is produced by the toolchain's own `leanexport` executable, so the export format matches the compiler that produced the {tech}[`.olean` files].
+
+The challenge author writes the {ref "lake-challenge-config"}[configuration file] in JSON format and distributes it with the challenge.
+Solutions are checked by using {lake}`challenge` with {lakeOptDef option}`--config=FILE`.
+
+The exit code distinguishes an accepted solution (`0`) and a rejected one (`1`) from an environment in which the judgment could not run at all (`2`).
+
+This command is a frontend to the [`comparator`](https://github.com/leanprover/comparator) proof-checking pipeline; {ref "validating-comparator"}[the section on validating proofs] describes the security model and the assumptions that remain.
+::::
+
+## Configuration
+%%%
+tag := "lake-challenge-config"
+%%%
+
+:::paragraph
+The challenge configuration is a JSON file that contains an object with the following keys:
+
+: `challenge_module` (required)
+
+  The name of the {tech}[challenge] module.
+
+: `solution_module` (required)
+
+  The name of the {tech}[solution] module to be checked.
+
+: `theorem_names` (required)
+
+  An array of theorem names.
+  These theorems should be complete in the solution, but {lean}`sorry` in the challenge.
+
+: `permitted_axioms` (required)
+
+  An array of axiom names that are permitted in the solution.
+
+: `definition_names`
+
+  An array of names of definitions that should be filled out in the solution.
+
+: `external_kernels`
+
+  An object in which each key names an external checker.
+  The value associated with the key is the command to be run, and must be a non-empty array of strings.
+  The first element in the array is the executable (found via {envVar}`PATH`), and the remaining elements are its arguments.
+
+  Each checker runs in the sandbox with one further argument appended to its command.
+  A checker whose name contains `noda` receives the path to a generated `nanoda`-style configuration file that specifies the export file and the permitted axioms, while every other checker receives the path to a file that contains the {tech}[solution]'s export.
+  A checker signals acceptance by exiting successfully, and the solution must be accepted by every configured checker in addition to Lean's kernel.
+
+: `enable_nanoda`
+
+  A Boolean for which `true` is equivalent to an `external_kernels` entry that maps `"nanoda"` to `["nanoda_bin"]`.
+  It may be `true` only when `external_kernels` is empty or omitted.
+
+:::
+
+## Sandbox
+
+:::paragraph
+The sandbox restricts only filesystem writes and outbound TCP connections:
+
+* Writes are confined to the project's `.lake` directory.
+* Only dependency resolution may open connections, on ports 443 and 22, the ports used by git's `https` and `ssh` transports.
+
+Reads, execution, and network traffic other than TCP are unrestricted.
+:::
+
+On Linux kernels that predate the Landlock fix released in Linux 7.1, `landrun` can be escaped through an `AF_UNIX` socket.
+Where that matters, run the command under a wrapper that removes the capability:
+
+```
+systemd-run --user --pty --property=RestrictAddressFamilies=~AF_UNIX \
+  lake challenge --config challenge.json
+```
+
 # Development Tools
 
 Lake includes support for specifying standard development tools and workflows.

Manual/Tactics/Reference.lean

@@ -302,7 +302,7 @@ tag := "tactic-ref-rw"
 :::tactic "erw"
 :::
 
-:::tactic Lean.Parser.Tactic.tacticRwa__
+:::tactic Lean.Parser.Tactic.rwa
 :::
 
 {docstring Lean.Meta.Rewrite.Config +allowMissing}

Manual/ValidatingProofs.lean

@@ -110,7 +110,7 @@ This command prints the set of axioms used by the theorem and the theorems it de
 The three axioms above are standard axioms of Lean's logic, and benign.
 
 * If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses {lean}`sorry` or is otherwise incomplete.
-* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion.
+* If axioms with {lit}`_native` in their names are reported, then {ref "validating-trustCompiler"}[native evaluation] is used.
 * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms.
 
 ## Trust
@@ -178,7 +178,8 @@ This should only be necessary for high risk scenarios (proof marketplaces, high-
 
 ## Instructions
 
-In a trusted environment, write the theorem *statement* (the “challenge”), and then feed the challenge as well as the proposed proof to the [`comparator`](https://github.com/leanprover/comparator) tool, with external checkers enabled, as documented there.
+In a trusted environment, write the theorem *statement* (the “challenge”), and then judge the proposed proof against it with {ref "lake-challenge"}[`lake challenge`], with external checkers enabled.
+This command is a frontend to the [`comparator`](https://github.com/leanprover/comparator) tool.
 
 ## Significance
 
@@ -227,11 +228,12 @@ This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +nati
 Specific uses wrapped in {tech}[honest] tactics (e.g. {tactic}`bv_decide`) are generally trustworthy.
 The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted.
 
-General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation.
+In general, native computation ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {lit}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation.
 In particular, for every {attr}`implemented_by`/{attr}`extern` attribute in libraries it becomes part of the trusted code base that the replacement is semantically equivalent.
 
-All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
+All these uses show up as an axiom {lit}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
 External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler.
 When that level of checking is needed, proofs have to avoid using native evaluation.
 
-Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use {name}`Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The {name}`Lean.trustCompiler` machinery is deprecated and will eventually be removed.
+Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics introduce one dedicated axiom for each computation that is asserted by native computation.
+The {lit}`Lean.trustCompiler` machinery was removed from Lean in version 4.35.0.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e9135801a2aeabf99ce43eb58e6331bd3afa1adc",
+   "rev": "796cfdb6eb682e191fb0ccc7da9de4b018dd7f0d",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "76f052847294d189dc9924a33466b4b677f47e67",
+   "rev": "6e558472c981dbee8cb9fcde92fa9593daf04228",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c271f30a1bf40c7292e1a82c9d5e6f3e389c23b3",
+   "rev": "3094dd5215be009cacc296f17356b395dc44d0f8",
    "name": "versowebcomponents",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669",
+   "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "847084e80500726e4331dded5f17007ddaf89c31",
+   "rev": "fda188f7329fa18ce4b2e8cc96c9b0a8f0c78c46",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-27
+leanprover/lean4:nightly-2026-08-31