[sorrachai]

Automatically attempt stable Lean upgrades and open a PR only after the candidate passes validation. Failed attempts open a tracking issue with the failed stage and run logs; review and merging remain manual.

• Check daily for the latest stable Lean 4 release and wait for matching Mathlib/CSLib tags whose toolchain files agree.
• Update the toolchain, both dependency pins and current README version examples, regenerate the manifest with Lake, and run the build, public import, declaration-checker and style checks. Verify that main has not advanced during validation before publishing.
• On success, open the upgrade PR and explicitly dispatch CI on its branch using the built-in token.
• On failure, open one issue per version. Later schedules skip that version; a manual retry is available. Failed retries add details to the same issue, and successful retries open a PR with a closing reference. Existing upgrade PRs, including maintainer fixes, are never refreshed or recreated.
• After a merge passes main-branch CI, publish a stable version tag and dated GitHub release at the tested commit. Existing tags remain fixed; README installation examples use v4.35.0.

Missing upstream releases wait quietly. Dependency, proof, tooling, base-change, publication and CI-dispatch failures are reported as failed attempts; the logs distinguish the cause. A passing build still needs public API and migration-note review.

Validation: 14 tests cover release selection, dependency readiness, existing PR/issue handling, retry behavior, failure reporting, atomic validation of file edits, numeric versions and prerelease exclusion. The actual workflow shell checks were tested with forbidden/precise imports and a local Git main branch that advances during validation. actionlint 1.7.12 and shell/YAML checks passed. A read-only live GitHub API run verified both the current-version no-op and matching-release selection; no upgrade PR or failure issue was created during validation. GitHub CI passed Build project (including public imports and checkdecls) and Lint style (including all 14 automation tests). Release publication was correctly skipped on the PR.

Setup: enable Settings → Actions → General → Workflow permissions → Allow GitHub Actions to create and approve pull requests. No extra secret or report-service registration is required. Configure main branch protection to require Build project and Lint style, with branches up to date before merging. This PR documents but does not change repository settings.

The scheduled updater and release publishing become active after merge.