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: