From f0e729b35ca468842d5dd81bb34d09aa6efb1577 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Sat, 4 Jul 2026 10:11:59 -0500
Subject: [PATCH] =?UTF-8?q?docs(citation):=20add=20pipeline-math=20?=
 =?UTF-8?q?=E2=80=94=20Peng=20et=20al.=20GPT-5.5=20Pro=20+=20Lean=20pipeli?=
 =?UTF-8?q?ne?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Same Erdős problem 477, same greedy algorithm, same Lean formalization
approach. Their prover-verifier pipeline mirrors SilverSight's autoresearch
(phi4 -> lake build). 95% Lean 4.
---
 CITATION.cff | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/CITATION.cff b/CITATION.cff
index 469574a6..66218ea4 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -398,6 +398,29 @@ references:
       formal/CoreFormalism/CRTSidon.lean.
     version: "accessed 27 June 2026"
 
+  - type: online
+    title: "Pipeline-Math: LLM-generated solutions to open problems"
+    authors:
+      - family-names: "Peng"
+        given-names: "Binghui"
+      - family-names: "Tao"
+        given-names: "Runzhou"
+      - family-names: "Wang"
+        given-names: "Steven"
+      - family-names: "Yu"
+        given-names: "Hantao"
+      - family-names: "Liu"
+        given-names: "Diyi"
+    date-published: "2026-06"
+    repository-code: "https://github.com/Pengbinghui/pipeline-math"
+    notes: >
+      GPT-5.5 Pro (prover) + Claude Code (assembler) pipeline producing
+      solutions to open problems (COLT, FOCS, Erdős, commutative ring theory)
+      with Lean 4 formalization. Solves Erdős Problem 477 (tiling complement)
+      — the same problem and greedy algorithm as SilverSight's crt_sidon_set.
+      Their prover-verifier pipeline mirrors SilverSight's autoresearch
+      (phi4/prove.py -> lake build verification). 95% of repo is Lean 4.
+
   - type: online
     title: "Toroidal and Poloidal Coordinates"
     authors: