diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index a2eb7343d0..dfcfef266f 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -62,42 +62,56 @@ jobs:
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
-      - name: Delete existing release if present
+      - name: Delete existing releases if present
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          # Try to delete any existing release for the current PR (just the version without the SHA suffix).
+          # Delete any existing releases for this PR.
+          # The short format release is always recreated with the latest commit.
+          # The SHA-suffixed release should be unique per commit, but delete just in case.
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
+          gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+      # Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action).
+      - name: Verify release artifacts exist
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          shopt -s nullglob
+          files=(artifacts/*/*)
+          if [ ${#files[@]} -eq 0 ]; then
+            echo "::error::No artifacts found matching artifacts/*/*"
+            exit 1
+          fi
+          echo "Found ${#files[@]} artifacts to upload:"
+          printf '%s\n' "${files[@]}"
+      # We use `gh release create` instead of `softprops/action-gh-release` because
+      # the latter enumerates all releases to check for existing ones, which fails
+      # when the repository has more than 10000 releases (GitHub API pagination limit).
+      # Upstream fix: https://github.com/softprops/action-gh-release/pull/725
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
-        with:
-          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          # There are coredumps files here as well, but all in deeper subdirectories.
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
-          draft: false
-          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
-          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        run: |
+          # There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives.
+          gh release create \
+            --repo ${{ github.repository_owner }}/lean4-pr-releases \
+            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \
+            --notes "" \
+            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \
+            artifacts/*/*
         env:
-          # The token used here must have `workflow` privileges.
-          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
-        with:
-          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
-          # There are coredumps files here as well, but all in deeper subdirectories.
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
-          draft: false
-          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
-          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        run: |
+          gh release create \
+            --repo ${{ github.repository_owner }}/lean4-pr-releases \
+            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \
+            --notes "" \
+            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \
+            artifacts/*/*
         env:
-          # The token used here must have `workflow` privileges.
-          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}