docs(citation): add pipeline-math — Peng et al. GPT-5.5 Pro + Lean pipeline

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.
This commit is contained in:
allaun 2026-07-04 10:11:59 -05:00
parent 8b49006810
commit f0e729b35c

View file

@ -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: