Bump lean v4.28.0 rc1

.devcontainer/Dockerfile

@@ -14,5 +14,5 @@ RUN apt-get update && \
 USER vscode
 WORKDIR /home/vscode
 
-RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.27.0-rc1
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.28.0-rc1
 ENV PATH="/home/vscode/.elan/bin:${PATH}"

AGENTS.md

@@ -0,0 +1,30 @@
+# AGENTS.md
+
+## Important Instructions
+
+- Use spaces only; never use tabs.
+- Do not modify `lakefile.toml`.
+- Do not use `python`, `cat`, `git checkout`, or `git reset`.
+- When encountering the error `expected '{' or indented tactic sequence`, fix the indentation.
+- Autonomously continue executing the tasks specified in `PLANS.md` until the maximum request limit is reached.
+- Use the `lean-lsp` MCP server tools when applicable.
+- Write all comments in English.
+- Use `$...$` or `$$...$$` for LaTeX math formatting in Markdown.
+- Always implement full proofs. Do not ask whether to proceed full proofs or introduce helper lemmas. If needed for full proofs, implement all of them.
+- Do not explore shorter proof paths before the current proof is completed. Only after completion may you consider improved approaches.
+- Before ending the session, run `lake build` to ensure the project builds successfully.
+
+## Prohibitions
+
+The following tokens are strictly prohibited to use in this project:
+
+- `sorry`
+- `admit`
+- `axiom`
+- `set_option`
+- `unsafe`
+- `System`
+- `open System`
+- `Lean.Elab`
+- `Lean.Meta`
+- `Lean.Compiler`

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Project",

lakefile.toml

@@ -16,4 +16,4 @@ name = "Project"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.27.0-rc1"
+rev = "v4.28.0-rc1"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.28.0-rc1