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