From a5cc1ed6eb19dfa76cb1c042b1b5148c3e7088a4 Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Fri, 18 Sep 2026 05:00:31 -0700 Subject: [PATCH] =?UTF-8?q?NOTICE.extra.yml:=20attribution=20for=20the=20E?= =?UTF-8?q?rd=C5=91s=E2=80=93S=C3=B3s=20(#548)=20import?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reproduces the upstream NOTICE of tadamcz/erdos548 (Apache License, Version 2.0, Section 4(d)) under LeanPool/Erdos548 and regenerates NOTICE, following the Köthe precedent in #409. Co-Authored-By: Claude Fable 5.1 --- NOTICE | 14 ++++++++++++++ NOTICE.extra.yml | 15 +++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/NOTICE b/NOTICE index eb9a41c65b..406ac061a5 100644 --- a/NOTICE +++ b/NOTICE @@ -339,6 +339,20 @@ files or LICENSE addenda. Only each project's Apache-2.0 Lean sources were imported here; these notes preserve attribution and citation requests made by the original authors. + LeanPool/Erdos548 https://github.com/tadamcz/erdos548 + The upstream repository ships a NOTICE file (Apache License, Version 2.0, + Section 4(d)). Its attribution notice reads: + + Erdős problem #548 (Erdős–Sós conjecture): proof + Copyright 2026 Tom Adamczewski / Epoch AI + + The formal statement was given to the AI system by the FrontierMath + Erdős benchmark of Tom Adamczewski and Thomas F. Bloom + (LeanOpenProblems, https://github.com/epoch-research/LeanOpenProblems, + commit 77882c437ca1dfefab3b27fa00f1d29788100311), Epoch AI, MIT License. + The Lean proofs were produced by a pre-release version of GPT-6 Astra + (OpenAI) running in that benchmark. + LeanPool/FormalLearningTheory https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel The upstream LICENSE appends a citation request. The original author asks that publications, software, or derivative works built on this diff --git a/NOTICE.extra.yml b/NOTICE.extra.yml index 9e9f9758e3..8ae824f240 100644 --- a/NOTICE.extra.yml +++ b/NOTICE.extra.yml @@ -37,6 +37,21 @@ DeadEnds: DirectedTopologyLean4: note: Copyright 2023 Dominique Lawson +Erdos548: + attribution: |- + The upstream repository ships a NOTICE file (Apache License, Version 2.0, + Section 4(d)). Its attribution notice reads: + + Erdős problem #548 (Erdős–Sós conjecture): proof + Copyright 2026 Tom Adamczewski / Epoch AI + + The formal statement was given to the AI system by the FrontierMath + Erdős benchmark of Tom Adamczewski and Thomas F. Bloom + (LeanOpenProblems, https://github.com/epoch-research/LeanOpenProblems, + commit 77882c437ca1dfefab3b27fa00f1d29788100311), Epoch AI, MIT License. + The Lean proofs were produced by a pre-release version of GPT-6 Astra + (OpenAI) running in that benchmark. + FactorizationSystems: note: Copyright (c) 2024 ivankobe