diff --git a/.github/workflows/first_bench_is_free.yml b/.github/workflows/first_bench_is_free.yml
new file mode 100644
index 00000000000000..bc236e8c673329
--- /dev/null
+++ b/.github/workflows/first_bench_is_free.yml
@@ -0,0 +1,25 @@
+name: Auto-bench
+
+on:
+  pull_request:
+    #types: [opened]  # This triggers the action when the PR is opened.
+
+jobs:
+  automatic_first_bench:
+    runs-on: ubuntu-latest
+
+    steps:
+
+      - name: Produce bench message
+        id: bench_message
+        run: |
+          message=$'!bench\n\nThis is an automated bench-marking that runs when a PR is opened. No need to repeat.\n'
+          printf '%s' "${message}" | hexdump -cC
+          printf 'message<<EOF\n%s\nEOF' "${message}" >> "${GITHUB_OUTPUT}"
+
+      - name: Add comment to PR
+        uses: GrantBirki/comment@v2
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          issue-number: ${{ github.event.pull_request.number }}
+          body: ${{ steps.bench_message.outputs.message }}
diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml
new file mode 100644
index 00000000000000..9fb6c45c37a634
--- /dev/null
+++ b/.github/workflows/zulip_api.yml
@@ -0,0 +1,54 @@
+name: Add "ready-to-merge" and "delegated" label
+
+# triggers the action when
+on:
+  push:
+  # the PR receives a comment
+  issue_comment:
+    types: [created]
+  # the PR receives a review
+  pull_request_review:
+    # whether or not it is accompanied by a comment
+    types: [submitted]
+  # the PR receives a review comment
+  pull_request_review_comment:
+    types: [created]
+
+jobs:
+  add_ready_to_merge_label:
+    # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not
+    # both set simultaneously: depending on the event that triggers the PR, usually only one is set
+    env:
+      AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
+      COMMENT_EVENT: ${{ github.event.comment.body }}
+      COMMENT_REVIEW: ${{ github.event.review.body }}
+    name: Add ready-to-merge or delegated label
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install zulip
+
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+        #  sparse-checkout: |
+        #    scripts/zulip_emoji_merge_delegate.py
+
+      - name: Run Zulip Emoji Merge Delegate Script
+        env:
+          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+          ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          printf 'cat scripts/zulip_emoji_merge_delegate.py\n'
+          cat scripts/zulip_emoji_merge_delegate.py
+          printf 'catted\n\n'
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
diff --git a/.github/workflows/zulip_emoji_merge_delegate.yaml b/.github/workflows/zulip_emoji_merge_delegate.yaml
deleted file mode 100644
index e44b4d07004d98..00000000000000
--- a/.github/workflows/zulip_emoji_merge_delegate.yaml
+++ /dev/null
@@ -1,35 +0,0 @@
-name: Zulip Emoji Merge Delegate
-
-on:
-  schedule:
-    - cron: '0 * * * *'  # Runs every hour
-
-jobs:
-  zulip-emoji-merge-delegate:
-    runs-on: ubuntu-latest
-
-    steps:
-    - name: Checkout mathlib repository
-      uses: actions/checkout@v4
-      with:
-        sparse-checkout: |
-          scripts
-
-    - name: Set up Python
-      uses: actions/setup-python@v5
-      with:
-        python-version: '3.x'
-
-    - name: Install dependencies
-      run: |
-        python -m pip install --upgrade pip
-        pip install zulip
-
-    - name: Run Zulip Emoji Merge Delegate Script
-      env:
-        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
-        ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
-        ZULIP_SITE: https://leanprover.zulipchat.com
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      run: |
-        python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$GITHUB_TOKEN"
diff --git a/Mathlib/New.lean b/Mathlib/New.lean
new file mode 100644
index 00000000000000..4ba280517af592
--- /dev/null
+++ b/Mathlib/New.lean
@@ -0,0 +1 @@
+--
diff --git a/zulip_emoji_merge_delegate.py b/zulip_emoji_merge_delegate.py
new file mode 100644
index 00000000000000..4d5582e226f67d
--- /dev/null
+++ b/zulip_emoji_merge_delegate.py
@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+import sys
+import zulip
+import re
+
+# Usage:
+# python scripts/zulip_emoji_merge_delegate.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $LABEL $PR_NUMBER
+# See .github/workflows/zulip_emoji_merge_delegate.yaml for the meaning of these variables
+
+ZULIP_API_KEY = sys.argv[1]
+ZULIP_EMAIL = sys.argv[2]
+ZULIP_SITE = sys.argv[3]
+LABEL = sys.argv[4]
+PR_NUMBER = sys.argv[5]
+
+print(f"LABEL: '{LABEL}'")
+print(f"PR_NUMBER: '{PR_NUMBER}'")
+
+# Initialize Zulip client
+client = zulip.Client(
+    email=ZULIP_EMAIL,
+    api_key=ZULIP_API_KEY,
+    site=ZULIP_SITE
+)
+
+# Fetch the last 200 messages
+response = client.get_messages({
+    "operator": "search",
+    "operand": f"https://github\.com/leanprover-community/mathlib4/pull/{PR_NUMBER}",
+})
+
+print(f"response: {response}")
+
+'''
+# messages = response['messages']
+for message in messages:
+    content = message['content']
+    print(f"matched: '{message}'")
+    # Check for emoji reactions
+    reactions = message['reactions']
+    has_peace_sign = any(reaction['emoji_name'] == 'peace_sign' for reaction in reactions)
+    has_bors = any(reaction['emoji_name'] == 'bors' for reaction in reactions)
+    has_merge = any(reaction['emoji_name'] == 'merge' for reaction in reactions)
+
+    pr_url = f"https://api.github.com/repos/leanprover-community/mathlib4/pulls/{PR_NUMBER}"
+
+    print('Removing peace_sign')
+    result = client.remove_reaction({
+        "message_id": message['id'],
+        "emoji_name": "peace_sign"
+    })
+    print(f"result: '{result}'")
+    print('Removing bors')
+    result = client.remove_reaction({
+        "message_id": message['id'],
+        "emoji_name": "bors"
+    })
+    print(f"result: '{result}'")
+
+    print('Removing merge')
+    result = client.remove_reaction({
+        "message_id": message['id'],
+        "emoji_name": "merge"
+    })
+    print(f"result: '{result}'")
+
+    if 'delegated' == LABEL:
+        print('adding delegated')
+
+        client.add_reaction({
+            "message_id": message['id'],
+            "emoji_name": "peace_sign"
+        })
+    elif 'ready-to-merge' == LABEL:
+        print('adding ready-to-merge')
+        if has_peace_sign:
+            client.remove_reaction({
+                "message_id": message['id'],
+                "emoji_name": "peace_sign"
+            })
+        client.add_reaction({
+            "message_id": message['id'],
+            "emoji_name": "bors"
+        })
+    elif LABEL.startswith("[Merged by Bors]"):
+        print('adding [Merged by Bors]')
+        if has_peace_sign:
+            client.remove_reaction({
+                "message_id": message['id'],
+                "emoji_name": "peace_sign"
+            })
+        if has_bors:
+            client.remove_reaction({
+                "message_id": message['id'],
+                "emoji_name": "bors"
+            })
+        client.add_reaction({
+            "message_id": message['id'],
+            "emoji_name": "merge"
+        })
+'''