diff --git a/FormalConjectures/Paper/DegreeSequencesTriangleFree.lean b/FormalConjectures/Paper/DegreeSequencesTriangleFree.lean
new file mode 100644
index 000000000..18c490b83
--- /dev/null
+++ b/FormalConjectures/Paper/DegreeSequencesTriangleFree.lean
@@ -0,0 +1,168 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+Title: Degree sequences in triangle-free graphs
+Authors: P. Erdős, S. Fajtlowicz and W. Staton,
+Published in Discrete Mathematics 92 (1991) 85–88.
+-/
+
+open BigOperators
+open Classical
+
+/-- A sequence of natural numbers is **compact** if consecutive terms at distance
+`2` differ by `1`. -/
+def IsCompactSequence (d : ℕ → ℕ) : Prop :=
+  ∀ k, d (k + 2) = d k + 1
+
+namespace SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- The number of vertices of `G` having degree `d`. -/
+noncomputable def degreeFreq (G : SimpleGraph α) (d : ℕ) : ℕ :=
+  (Finset.univ.filter fun v : α => G.degree v = d).card
+
+/-- `δ G` is the minimum degree of `G`. -/
+noncomputable def δ (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
+  sInf (Set.range fun v : α => G.degree v)
+
+end SimpleGraph
+
+section lemmas
+
+variable (d : ℕ → ℕ) (n k r : ℕ)
+
+/-- **Lemma 1 (a)** -/
+@[category research solved, AMS 5]
+lemma lemma1_a
+    (h_no_three : ∀ k, d (k + 2) ≠ d k) :
+    1 ≤ d (k + 2) - d k := by
+  sorry
+
+/-- **Lemma 1 (b)** -/
+@[category research solved, AMS 5]
+lemma lemma1_b
+    (h_no_three : ∀ i, d (i + 2) ≠ d i) :
+    r ≤ d (k + 2 * r) - d k := by
+  sorry
+
+/-- **Lemma 2 (a)** -/
+@[category research solved, AMS 5]
+lemma lemma2_a
+    (h_no_three : ∀ i, d (i + 2) ≠ d i) :
+    2 * n * n ≤
+      (∑ i ∈ Finset.Icc (2 * n + 1) (4 * n), d i) -
+        (∑ i ∈ Finset.Icc 1 (2 * n), d i) := by
+  sorry
+
+/-- **Lemma 2 (b)** -/
+@[category research solved, AMS 5]
+lemma lemma2_b
+    (h_no_three : ∀ i, d (i + 2) ≠ d i) :
+    2 * n * n + 2 * n + 1 ≤
+      (∑ i ∈ Finset.Icc (2 * n + 1) (4 * n + 1), d i) -
+        (∑ i ∈ Finset.Icc 1 (2 * n), d i) := by
+  sorry
+
+/-- **Lemma 2 (c)** -/
+@[category research solved, AMS 5]
+lemma lemma2_c
+    (h_no_three : ∀ i, d (i + 2) ≠ d i) :
+    2 * n * n + 2 * n ≤
+      (∑ i ∈ Finset.Icc (2 * n + 2) (4 * n + 2), d i) -
+        (∑ i ∈ Finset.Icc 1 (2 * n + 1), d i) := by
+  sorry
+
+/-- **Lemma 2 (d)** -/
+@[category research solved, AMS 5]
+lemma lemma2_d
+    (h_no_three : ∀ i, d (i + 2) ≠ d i) :
+    2 * n * n + 4 * n + 2 ≤
+      (∑ i ∈ Finset.Icc (2 * n + 2) (4 * n + 3), d i) -
+        (∑ i ∈ Finset.Icc 1 (2 * n + 1), d i) := by
+  sorry
+
+end lemmas
+
+namespace SimpleGraph
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+/-- The degree sequence of a graph, sorted in nondecreasing order. -/
+noncomputable def degreeSequence (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ :=
+  (Finset.univ.val.map fun v : α => G.degree v).sort (· ≤ ·)
+
+/-- The degree sequence of `G` is **compact** if it satisfies
+`IsCompactSequence`. -/
+def degreeSequenceCompact (G : SimpleGraph α) [DecidableRel G.Adj] : Prop :=
+  IsCompactSequence fun k => (degreeSequence G).getD k 0
+
+/-- **Theorem 1.** If a triangle-free graph has `f = 2`,
+then it is bipartite, has minimum degree `1`, and
+its degree sequence is compact. -/
+@[category research solved, AMS 5]
+theorem theorem1 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (h₂ : f G = 2) :
+    G.IsBipartite ∧ δ G = 1 ∧ degreeSequenceCompact G := by
+  sorry
+
+/-- **Lemma 3.** For every `n` there exists a bipartite graph with
+`8 n` vertices, minimum degree `n + 1`, and `f = 3`. -/
+@[category research solved, AMS 5]
+lemma lemma3 (n : ℕ) (hn : 0 < n) :
+    ∃ (G : SimpleGraph (Fin (8 * n))) (_ : DecidableRel G.Adj),
+      G.IsBipartite ∧ δ G = n + 1 ∧ f G = 3 := by
+  sorry
+
+/-- **Lemma 4.** A triangle-free graph can be extended by one to a
+triangle-free graph whose new part has minimum degree at least
+`2 n` and `f = 3`. -/
+@[category research solved, AMS 5]
+lemma lemma4 (G : SimpleGraph α) [DecidableRel G.Adj] (h₁ : G.CliqueFree 3) (v : α) :
+    ∃ (β : Type*) (_ : Fintype β) (H : SimpleGraph β) (_ : DecidableRel H.Adj) (i : α ↪ β),
+      (∀ u w, G.Adj u w ↔ H.Adj (i u) (i w)) ∧
+      H.degree (i v) = G.degree v + 1 ∧
+      (∀ w ≠ v, H.degree (i w) = G.degree w) ∧
+      let J := H.induce (Set.compl (Set.range i))
+      J.CliqueFree 3 ∧ f J = 3 ∧ δ J ≥ 2 * Fintype.card α := by
+  sorry
+
+/-- **Theorem 2.** Every triangle-free graph is an induced subgraph of one
+with `f = 3`. -/
+@[category research solved, AMS 5]
+theorem theorem2 (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.CliqueFree 3) :
+    ∃ (β : Type*) (_ : Fintype β) (H : SimpleGraph β) (_ : DecidableRel H.Adj) (i : α ↪ β),
+      (∀ u w, G.Adj u w ↔ H.Adj (i u) (i w)) ∧ H.CliqueFree 3 ∧ f H = 3 := by
+  sorry
+
+/-- `F n` is the smallest number of vertices of a triangle-free graph
+with chromatic number `n` and `f = 3`. -/
+@[category research solved, AMS 5]
+noncomputable def F (n : ℕ) : ℕ :=
+  sInf { p | ∃ (G : SimpleGraph (Fin p)) (_ : DecidableRel G.Adj),
+    G.CliqueFree 3 ∧ G.chromaticNumber = n ∧ f G = 3 }
+
+@[category research solved, AMS 5]
+theorem F_three : F 3 = 7 := by
+  sorry
+
+@[category research solved, AMS 5]
+theorem F_four_le : F 4 ≤ 19 := by
+  sorry
+
+end SimpleGraph
diff --git a/scripts/README.md b/scripts/README.md
new file mode 100644
index 000000000..2b219b6f2
--- /dev/null
+++ b/scripts/README.md
@@ -0,0 +1,15 @@
+# Codex helper
+
+The `run_single_file.py` script runs Codex inside Docker on a single file from this repository. It builds both `private_mathlib4` and `formal_conjectures` before invoking Codex. When using the `--prep` option you must also provide `--pr` so `prepare_single_file.py` can fetch review comments for that pull request.
+
+Example:
+
+```bash
+GEMINI_API_KEY="" ./scripts/run_single_file.py \
+  --prep FormalConjectures/Paper/CasasAlvero.lean \
+  --pr https://github.com/OWNER/REPO/pull/123 \
+  --export FormalConjectures/Paper/CasasAlvero.lean \
+  run --auto-continuous --auto-continuous-first-doc \
+  "lake build FormalConjectures/Paper/CasasAlvero.lean"
+```
+
diff --git a/scripts/prepare_single_file.py b/scripts/prepare_single_file.py
new file mode 100644
index 000000000..e8b1806bd
--- /dev/null
+++ b/scripts/prepare_single_file.py
@@ -0,0 +1,176 @@
+import argparse
+import os
+import json
+import shutil
+import re
+from typing import Dict, List
+
+import requests
+
+from scripts.split_conjecture_tasks import parse_stubs, lean_explore_search
+
+
+def fetch_pr_comments(pr_url: str, token: str | None = None) -> List[dict]:
+    """Return PR review comments from GitHub."""
+    m = re.match(r"https://github.com/(?P<owner>[^/]+)/(?P<repo>[^/]+)/pull/(?P<num>\d+)", pr_url)
+    if not m:
+        raise ValueError("Invalid PR URL")
+    owner = m.group('owner')
+    repo = m.group('repo')
+    num = m.group('num')
+    headers = {'Accept': 'application/vnd.github+json'}
+    if token:
+        headers['Authorization'] = f'Bearer {token}'
+
+    comments: List[dict] = []
+    page = 1
+    while True:
+        resp = requests.get(
+            f"https://api.github.com/repos/{owner}/{repo}/pulls/{num}/comments",
+            headers=headers,
+            params={'per_page': 100, 'page': page},
+        )
+        if resp.status_code != 200:
+            raise RuntimeError(f"GitHub API error: {resp.status_code} {resp.text}")
+        data = resp.json()
+        if not data:
+            break
+        comments.extend(data)
+        page += 1
+    return comments
+
+
+def insert_review_comments(path: str, comments: List[dict]) -> None:
+    """Insert review comments as docstrings in the file at *path*."""
+    if not comments:
+        return
+    with open(path, 'r') as fh:
+        lines = fh.readlines()
+
+    comments_by_line: Dict[int, List[str]] = {}
+    for c in comments:
+        line_no = c.get('original_line') or c.get('line')
+        if line_no is None:
+            continue
+        body = c.get('body')
+        if not body:
+            continue
+        comments_by_line.setdefault(int(line_no), []).append(body)
+
+    for line_no in sorted(comments_by_line.keys(), reverse=True):
+        bodies = comments_by_line[line_no]
+        for body in bodies[::-1]:
+            prefix = "-- REVIEW COMMENT: "
+            for i, line in enumerate(body.splitlines()):
+                if i == 0:
+                    lines.insert(line_no, prefix + line + "\n")
+                else:
+                    lines.insert(line_no + i, "-- " + line + "\n")
+
+    with open(path, 'w') as fh:
+        fh.writelines(lines)
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description="Prepare single Lean file task")
+    parser.add_argument('--lean', required=True, help='Lean file to process')
+    parser.add_argument('--out', required=True, help='Output directory')
+    parser.add_argument('--pool', default='docs/definitions_pool.json',
+                        help='Global pool of definitions')
+    parser.add_argument('--lean-explore', dest='lean_explore', default=None,
+                        help='LeanExplore API base URL')
+    parser.add_argument('--lean-explore-key', dest='lean_explore_key', default=None,
+                        help='LeanExplore API key')
+    parser.add_argument('--lean-explore-local', dest='lean_explore_local',
+                        action='store_true', help='Use LeanExplore local dataset')
+    parser.add_argument('--pr', dest='pull_request', required=True,
+                        help='GitHub pull request URL to fetch comments from')
+    parser.add_argument('--gh-token', dest='github_token', default=None,
+                        help='GitHub token for API access')
+    args = parser.parse_args()
+
+    os.makedirs(args.out, exist_ok=True)
+
+    local_service = None
+    if args.lean_explore_local:
+        try:
+            from lean_explore.local.service import Service
+            local_service = Service()
+        except Exception:
+            local_service = None
+
+    stubs = parse_stubs(args.lean)
+
+    pool = {}
+    if os.path.exists(args.pool):
+        with open(args.pool) as fh:
+            pool = json.load(fh)
+
+    def merge_def(name: str, definition: str) -> None:
+        current = pool.get(name)
+        if current is None:
+            pool[name] = definition
+        elif isinstance(current, list):
+            if definition not in current:
+                current.append(definition)
+        else:
+            if definition != current:
+                pool[name] = [current, definition]
+
+    for name, definition in stubs.items():
+        merge_def(name, definition)
+
+    with open(args.pool, 'w') as fh:
+        json.dump(pool, fh, indent=2, sort_keys=True)
+
+    # fetch PR comments and insert them into a copy of the file
+    pr_comments = fetch_pr_comments(args.pull_request, args.github_token)
+    relevant_comments = [c for c in pr_comments if os.path.normpath(c.get('path', '')) == os.path.normpath(args.lean)]
+    copied_file = os.path.join(args.out, os.path.basename(args.lean))
+    shutil.copy(args.lean, copied_file)
+    insert_review_comments(copied_file, relevant_comments)
+
+    with open(os.path.join(args.out, 'task.md'), 'w') as f_task:
+        f_task.write(f"# Task for {os.path.basename(args.lean)}\n\n")
+        f_task.write("Implement the following definitions and address reviewer comments.\n\n")
+        for d, code in stubs.items():
+            f_task.write(f"## {d}\n")
+            f_task.write("```lean\n" + code + "\n```\n")
+            for ref in lean_explore_search(
+                d,
+                args.lean_explore,
+                args.lean_explore_key,
+                backend='local' if args.lean_explore_local else 'remote',
+                service=local_service,
+            ):
+                code_snip = ref.get('code')
+                path = ref.get('file')
+                start = ref.get('start')
+                end = ref.get('end')
+                if code_snip:
+                    f_task.write(
+                        f"LeanExplore reference `{path}` lines {start}-{end}:\n")
+                    f_task.write("```lean\n" + code_snip + "\n```\n")
+                elif path:
+                    f_task.write(
+                        f"-- LeanExplore reference: {path} lines {start}-{end}\n")
+            f_task.write("\n")
+
+    with open(os.path.join(args.out, 'AGENTS_single_task.md'), 'w') as f_agent:
+        f_agent.write("# Single File Task\n\n")
+        f_agent.write(f"Work on `{args.lean}`. Implement the missing definitions and incorporate the reviewer comments added to the file.\n\n")
+        f_agent.write("1. Fill in the missing definitions.\n")
+        f_agent.write(f"2. Run `lake build {args.lean}` and ensure it compiles.\n")
+        f_agent.write("3. Do not delete existing code.\n")
+        f_agent.write("4. Use `python3 scripts/local_search_tool.py <string> --limit 5` to find additional Lean and mathlib references.\n")
+        f_agent.write("   For example:\n   `python3 scripts/local_search_tool.py \"bipartite graph\" --limit 5`\n")
+        f_agent.write("5. Deleting the theorem or definitions is not allowed.\n")
+        f_agent.write("6. Work until the compilation succeeds. Do not give up.\n")
+        f_agent.write("7. If patching does not work then write the file from scratch, using for example `cat > {args.lean} << 'EOF'`.\n")
+        f_agent.write("8. You work in a sandbox. Simple commands such as `lake build` are going to work, but hacking the manifest or rebuilding the whole of mathlib is unlikely to succeed. Focus on simple changes.\n")
+        f_agent.write("9. It is not allowed to leave definitions and theorems inside a docstring / comment, because you need to check whether they can be compiled with `lake build`.\n")
+        f_agent.write("10. Ensure reviewer comments have been addressed in your implementation.\n")
+
+
+if __name__ == '__main__':
+    main()
diff --git a/scripts/run_single_file.py b/scripts/run_single_file.py
new file mode 100755
index 000000000..50032bcfc
--- /dev/null
+++ b/scripts/run_single_file.py
@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""Run Codex inside Docker on a single file from the Formal Conjectures repo.
+
+This helper mirrors ``run_in_container_single_file.sh`` but defaults to
+``/opt/lean_pkgs/private_conjectures`` as the working repository and ensures
+both this repository and ``private_mathlib4`` are built before Codex runs.
+"""
+
+import argparse
+import os
+import shlex
+import subprocess
+import sys
+
+
+def parse_args() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(description="Run Codex in Docker")
+    parser.add_argument("--image", default="codex_patched", help="Docker image tag")
+    parser.add_argument("--name", help="Container name (default: script-<pid>)")
+    parser.add_argument("--prep", help="Prepare a single Lean file")
+    parser.add_argument(
+        "--pr",
+        dest="pull_request",
+        help="GitHub pull request URL used when preparing a file",
+    )
+    parser.add_argument(
+        "--gh-token",
+        dest="github_token",
+        default=None,
+        help="GitHub token for API access when preparing a file",
+    )
+    parser.add_argument(
+        "--export", action="append", default=[], help="Files to export from container"
+    )
+    parser.add_argument(
+        "cmd", nargs=argparse.REMAINDER, help="Command run inside Codex"
+    )
+    args = parser.parse_args()
+    if not args.cmd:
+        parser.error("Need Codex command")
+    if args.prep and not args.pull_request:
+        parser.error("--prep requires --pr")
+    return args
+
+
+def docker(*args, check=True, capture_output=False, text=True):
+    return subprocess.run(
+        ["docker", *args], check=check, capture_output=capture_output, text=text
+    )
+
+
+def main() -> int:
+    args = parse_args()
+    repo = "/opt/lean_pkgs/private_conjectures"
+    cname = args.name or f"pc-{os.getpid()}"
+    dummy_key = "sk-0123456789abcdef0123456789abcdef0123456789ab"
+    allowed_domains = [
+        "huggingface.co",
+        "cdn-lfs.huggingface.co",
+        "cdn-lfs.hf.co",
+        "generativelanguage.googleapis.com",
+        "releases.lean-lang.org",
+        "api.github.com",
+        "github.com",
+        "codeload.github.com",
+        "raw.githubusercontent.com",
+        "objects.githubusercontent.com",
+    ]
+
+    result = docker(
+        "run",
+        "-d",
+        "--name",
+        cname,
+        "--cap-add=NET_ADMIN",
+        "--cap-add=NET_RAW",
+        "--security-opt",
+        "seccomp=unconfined",
+        "-e",
+        "HOME=/home/node",
+        "-e",
+        f"OPENAI_API_KEY={dummy_key}",
+        *(
+            ["-e", f"GEMINI_API_KEY={os.environ['GEMINI_API_KEY']}"]
+            if "GEMINI_API_KEY" in os.environ
+            else []
+        ),
+        args.image,
+        "sleep",
+        "infinity",
+        capture_output=True,
+    )
+    cid = result.stdout.strip()
+
+    try:
+        docker("exec", "--user", "root", cid, "chown", "-R", "1000:1000", repo)
+        docker(
+            "exec",
+            "--user",
+            "root",
+            cid,
+            "bash",
+            "-c",
+            "mkdir -p /etc/codex && "
+            + "printf '%s\n' "
+            + " ".join(allowed_domains)
+            + " > /etc/codex/allowed_domains.txt && "
+            + "chmod 444 /etc/codex/allowed_domains.txt && /usr/local/bin/init_firewall.sh",
+        )
+
+        if args.prep:
+            prep_cmd = (
+                f"python3 -m scripts.prepare_single_file --lean {shlex.quote(args.prep)} "
+                f"--out tmp_prep --lean-explore-local --pr {shlex.quote(args.pull_request)}"
+            )
+            if args.github_token:
+                prep_cmd += f" --gh-token {shlex.quote(args.github_token)}"
+            docker(
+                "exec",
+                cid,
+                "bash",
+                "-euc",
+                f"cd {repo} && {prep_cmd} && "
+                f"cp tmp_prep/AGENTS_single_task.md AGENTS.md && "
+                f"cp tmp_prep/$(basename {args.prep}) {args.prep}",
+            )
+
+        docker(
+            "exec",
+            "-it",
+            cid,
+            "bash",
+            "-c",
+            "cd /opt/lean_pkgs/private_mathlib4 && lake build FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean",
+        )
+        docker(
+            "exec",
+            "-it",
+            cid,
+            "bash",
+            "-c",
+            "cd /opt/lean_pkgs/private_conjectures && lake build FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean",
+        )
+        if args.prep:
+            docker(
+                "exec",
+                "-it",
+                cid,
+                "bash",
+                "-c",
+                f"cd /opt/lean_pkgs/private_conjectures && lake build {args.prep}",
+            )
+
+        quoted = " ".join(shlex.quote(c) for c in args.cmd)
+        docker(
+            "exec",
+            "-it",
+            cid,
+            "env",
+            f"OPENAI_ALLOWED_DOMAINS={' '.join(allowed_domains)}",
+            "env",
+            "LAKE_PKGS_DISABLE_AUTO_UPDATE=1",
+            *(
+                ["env", f"GEMINI_API_KEY={os.environ['GEMINI_API_KEY']}"]
+                if "GEMINI_API_KEY" in os.environ
+                else []
+            ),
+            "bash",
+            "-euo",
+            "pipefail",
+            "-c",
+            f"cd {repo} && codex --provider=gemini --full-auto --model=gemini-2.5-pro {quoted}",
+        )
+
+        for path in args.export:
+            host_dir = os.path.join(".", os.path.splitext(os.path.basename(path))[0])
+            os.makedirs(host_dir, exist_ok=True)
+            check = subprocess.run(
+                ["docker", "exec", cid, "test", "-e", f"{repo}/{path}"]
+            )
+            if check.returncode == 0:
+                docker("cp", f"{cid}:{repo}/{path}", host_dir + "/")
+                print(f"\u2714 copied {path}")
+            else:
+                print(f"\u26a0 {path} not found in container")
+
+    finally:
+        subprocess.run(
+            ["docker", "rm", "-f", cid],
+            stdout=subprocess.DEVNULL,
+            stderr=subprocess.DEVNULL,
+        )
+
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())