NOTICE.extra.yml: attribution for the Köthe disproof import

.github/workflows/docs.yml

@@ -19,6 +19,11 @@ on:
       - main
     paths:
       - 'README.md'
+      # Attribution-only and CI-only PRs must still produce the required
+      # `Documentation preflight` check.
+      - 'NOTICE.extra.yml'
+      - '.github/workflows/lean_action_ci.yml'
+      - 'scripts/ci/**'
       - '**/*.lean'
       - 'LeanPool/projects.yml'
       - 'Challenge/challenges.yml'

.github/workflows/lean_action_ci.yml

@@ -51,6 +51,8 @@ on:
       - 'bump/**'
     paths:
       - 'README.md'
+      # Attribution-only PRs must still produce the required checks.
+      - 'NOTICE.extra.yml'
       - '**/*.lean'
       - 'lakefile.toml'
       - 'lean-toolchain'

NOTICE

@@ -333,6 +333,25 @@ the original authors.
           of the Fundamental Theorem of Statistical Learning.
           https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel
 
+  LeanPool/Koethe                    https://github.com/tadamcz/koethe
+      The upstream repository ships a NOTICE file (Apache License, Version 2.0,
+      Section 4(d)). Its attribution notice reads:
+
+          Köthe conjecture: disproof (Krempa's matrix form)
+          Copyright 2026 Tom Adamczewski / Epoch AI
+
+          This repository includes a definition and a conjecture statement copied
+          from Formal Conjectures (https://github.com/google-deepmind/formal-conjectures,
+          file FormalConjectures/Wikipedia/Koethe.lean at commit
+          9cbe1d3c12998c786b7c2cd99ce28a21b6631f66), Copyright 2025 The Formal
+          Conjectures Authors, licensed under the Apache License, Version 2.0.
+
+          The formal statement was given to the AI system by Epoch AI's
+          LeanOpenProblems harness (https://github.com/epoch-research/LeanOpenProblems,
+          branch wikipedia-dataset, commit 0ef96d7b12cfa96a93761b4bba1c635f4546c5ca),
+          MIT License. The Lean proof was produced by a pre-release version of
+          GPT-6 Astra (OpenAI) running in that harness.
+
   LeanPool/ZhangYeungInequality      https://github.com/cboone/zhang-yeung-inequality
       The upstream repository ships a NOTICE file (Apache License, Version 2.0,
       Section 4(d)). Its attribution notice reads:

NOTICE.extra.yml

@@ -70,6 +70,26 @@ GrothendieckVanishing:
     Attribution-NonCommercial-ShareAlike 4.0 International license, then
     relicensed under the Apache License, Version 2.0, by its sole author.
 
+Koethe:
+  attribution: |-
+    The upstream repository ships a NOTICE file (Apache License, Version 2.0,
+    Section 4(d)). Its attribution notice reads:
+
+        Köthe conjecture: disproof (Krempa's matrix form)
+        Copyright 2026 Tom Adamczewski / Epoch AI
+
+        This repository includes a definition and a conjecture statement copied
+        from Formal Conjectures (https://github.com/google-deepmind/formal-conjectures,
+        file FormalConjectures/Wikipedia/Koethe.lean at commit
+        9cbe1d3c12998c786b7c2cd99ce28a21b6631f66), Copyright 2025 The Formal
+        Conjectures Authors, licensed under the Apache License, Version 2.0.
+
+        The formal statement was given to the AI system by Epoch AI's
+        LeanOpenProblems harness (https://github.com/epoch-research/LeanOpenProblems,
+        branch wikipedia-dataset, commit 0ef96d7b12cfa96a93761b4bba1c635f4546c5ca),
+        MIT License. The Lean proof was produced by a pre-release version of
+        GPT-6 Astra (OpenAI) running in that harness.
+
 LatticeTriangle:
   note: Copyright (c) 2026 Axiom Math