NOTICE.extra.yml: attribution for the Köthe disproof import by Vilin97 · Pull Request #409 · LeanPool/lean-pool

Vilin97 · 2026-09-10T19:10:16Z

Non-content companion to #408, stacked on that branch (base: claude/daily-import-koethe-2026-09-10) and kept as a draft until #408 merges.

Adds the Koethe: attribution block to NOTICE.extra.yml, reproducing the upstream repository's NOTICE (Apache License 2.0, §4(d)): copyright Tom Adamczewski / Epoch AI, the vendored Formal Conjectures statement (© The Formal Conjectures Authors, Apache-2.0), and the LeanOpenProblems harness (MIT), and regenerates NOTICE with python -m lean_pool.notice --repo .. (13 notice tests pass on this branch).

Why stacked: the NOTICE generator (and tests/test_notice.py) rejects notes for projects that are not registered in LeanPool/projects.yml, so this entry cannot land on main before the project card does, and the content-PR guard forbids bundling it with #408. Once #408 is squash-merged, retarget this PR to main, refresh the branch, rerun the generator (the metadata workflow will have regenerated NOTICE without the attribution in between), and merge.

🤖 Generated with Claude Code

Imports tadamcz/koethe at a94a72aec957cb28d76aa30fb97a01d440990d7f (Apache-2.0): a machine-checked counterexample to Krempa's matrix form of Köthe's 1930 conjecture, found autonomously by GPT-6 Astra in Epoch AI's LeanOpenProblems harness and written up in arXiv:2609.07996. The single upstream file is split into modules along its own part boundaries, the broad `import Mathlib` is replaced by minimal imports, the per-part `set_option autoImplicit false` lines are dropped, the pencil field `constant` is renamed `scalar`, and the Mathlib API drift from v4.28.0 to v4.34.0-rc1 is repaired (structure-based `MvPolynomial`, antidiagonal and height lemma renames, `Fintype` sums over structure fields). No statement is weakened; three auxiliary lemmas are generalized from `Fintype` to `Finite` index types. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

…wski / Epoch AI) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

… import The Köthe project (#408) is Apache-2.0 with a NOTICE file naming Tom Adamczewski / Epoch AI, the vendored Formal Conjectures statement, and the LeanOpenProblems harness. Apache-2.0 §4(d) asks that this attribution be carried along; NOTICE itself is regenerated by the metadata workflow once the project card lands. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

greptile-apps · 2026-09-10T19:13:38Z

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

The PR appears safe to merge because no blocking failure remains.

Summary

Records the upstream copyright, Formal Conjectures provenance, and LeanOpenProblems harness attribution.
Regenerates the corresponding Köthe section in NOTICE.
Adds NOTICE.extra.yml to Lean and documentation workflow path filters and includes selected CI inputs in the documentation filter.

_{Reviews (10) · Last reviewed commit: "ci: also run Documentation preflight on ..."}

github-actions · 2026-09-10T19:26:53Z

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

github-actions · 2026-09-10T22:05:32Z

Auto-rebase stopped: this PR conflicts with main outside the two
mechanically resolvable files (LeanPool.lean, LeanPool/projects.yml),
so the overlap needs a human. Remove the needs-manual-rebase label once
resolved to re-enable automatic updates.

… main)

…attribution

Vilin97 · 2026-09-11T02:25:45Z

Automation disposition: needs-maintainer (reviewed and correct; required checks cannot run on a NOTICE-only diff)

Reviewed exact head 0e8249f7fcc4f8f453d48783ff80804cad9ec400 (base retargeted to main after #408 merged; the branch was re-merged with main taking main's Lean files and NOTICE regenerated with python -m lean_pool.notice). The diff against main is exactly NOTICE (+19) and NOTICE.extra.yml (+20): the Apache-2.0 §4(d) attribution block for LeanPool/Koethe reproducing the upstream tadamcz/koethe NOTICE (Tom Adamczewski / Epoch AI, the vendored Formal Conjectures statement, the MIT-licensed LeanOpenProblems harness). Content / non-content separation and Python CI (13 notice tests) pass on this head; the obsolete Greptile thread from the stacked phase is resolved.

Why it is not merged. Branch protection requires Build project and Documentation preflight, but lean_action_ci.yml and docs.yml only trigger on pull_request for Lean/Lake/metadata paths — NOTICE* is not among them — so neither check is ever created for this PR. I ran both workflows on this head with workflow_dispatch (runs 2026-09-11 01:53 UTC, both green), but GitHub does not count workflow_dispatch check runs toward a pull request's status rollup, so the PR stays BLOCKED. Merging would need an admin bypass, which automation does not use.

Decision for the maintainer (one of): (a) admin-merge this PR; (b) add NOTICE / NOTICE.extra.yml to the pull_request.paths of lean_action_ci.yml and docs.yml so attribution PRs get the required checks (a CI change, outside automation scope), then re-run; or (c) land the attribution block through the generated-metadata workflow directly on main.

Branch protection requires Build project and Documentation preflight, but neither workflow triggered on attribution-only diffs, so a NOTICE.extra.yml PR could never be merged without an admin bypass. Add the file to both pull_request path filters; the push filters are unchanged. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Vilin97 · 2026-09-11T06:58:35Z

Maintainer decision received: merge. An admin bypass is not something this automation performs, so the other route from the 2026-09-11 02:25 UTC comment was taken instead: commit 5ac7a62f adds NOTICE.extra.yml to the pull_request path filters of lean_action_ci.yml and docs.yml (push filters unchanged), so attribution-only PRs produce the required Build project and Documentation preflight checks from now on. main merged in (5ef7012b), NOTICE verified canonical with python -m lean_pool.notice --check. Merging once the required checks report green.

github-actions · 2026-09-11T07:16:34Z

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

…anges PR #412 changes only lean_action_ci.yml and scripts/ci/plan-build-shards.py, so docs.yml never triggered and the required Documentation preflight check could not be created. List those paths as well. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

github-actions · 2026-09-11T09:06:30Z

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

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: Vilin97 automation <automation@lean-pool.local> Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>

Vilin97 and others added 4 commits September 10, 2026 12:04

Match file headers to the upstream NOTICE copyright line (Tom Adamcze…

f2200ee

…wski / Epoch AI) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Regenerate NOTICE with the Köthe attribution

e8c9a5a

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Vilin97 marked this pull request as draft September 10, 2026 19:10

Vilin97 force-pushed the claude/koethe-notice-attribution branch from ef982da to e8c9a5a Compare September 10, 2026 19:10

Vilin97 changed the base branch from main to claude/daily-import-koethe-2026-09-10 September 10, 2026 19:11

greptile-apps Bot reviewed Sep 10, 2026

View reviewed changes

Comment thread NOTICE.extra.yml

Merge remote-tracking branch 'origin/main' into pr-409

e7d6323

Vilin97 mentioned this pull request Sep 10, 2026

Import the disproof of the Köthe conjecture (Krempa's matrix form) #408

Merged

Vilin97 mentioned this pull request Sep 10, 2026

Formalization imported into Lean Pool tadamcz/koethe#2

Open

Vilin97 changed the base branch from claude/daily-import-koethe-2026-09-10 to main September 10, 2026 22:08

Vilin97 marked this pull request as ready for review September 10, 2026 22:08

Vilin97 and others added 6 commits September 10, 2026 15:31

Merge main into the NOTICE attribution branch (Köthe files taken from…

22eb9ff

… main)

Merge remote-tracking branch 'origin/main' into pr-409

ce1c308

Merge remote-tracking branch 'origin/main' into pr-409

7ee0486

Merge remote-tracking branch 'origin/main' into pr-409

43a343b

Merge remote-tracking branch 'origin/main' into pr-409

4b409c1

Merge remote-tracking branch 'origin/main' into claude/koethe-notice-…

0e8249f

…attribution

Vilin97 added the needs-maintainer Actual human decision required: licensing, mathematical scope, policy, or reviewer disagreement. label Sep 11, 2026

github-actions Bot and others added 3 commits September 11, 2026 06:48

Merge remote-tracking branch 'origin/main' into pr-409

21beb1c

Merge remote-tracking branch 'origin/main' into fix-20260911/pr409

5ef7012

Vilin97 removed the needs-maintainer Actual human decision required: licensing, mathematical scope, policy, or reviewer disagreement. label Sep 11, 2026

Vilin97 merged commit 659990f into main Sep 11, 2026
16 checks passed

This was referenced Sep 18, 2026

Import the Erdős–Sós conjecture proof (Erdős Problem 548) #452

Merged

NOTICE.extra.yml: attribution for the Erdős–Sós (#548) import #453

Merged

Navigation Menu

Repository navigation

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

NOTICE.extra.yml: attribution for the Köthe disproof import#409
Vilin97 merged 15 commits into
mainfrom
claude/koethe-notice-attribution

Vilin97 commented Sep 10, 2026 •

edited

Loading

Uh oh!

greptile-apps Bot commented Sep 10, 2026 •

edited

Loading

Uh oh!

Uh oh!

github-actions Bot commented Sep 10, 2026

Uh oh!

github-actions Bot commented Sep 10, 2026

Uh oh!

Vilin97 commented Sep 11, 2026

Uh oh!

Vilin97 commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

Vilin97 commented Sep 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

greptile-apps Bot commented Sep 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

Uh oh!

github-actions Bot commented Sep 10, 2026

Uh oh!

github-actions Bot commented Sep 10, 2026

Uh oh!

Vilin97 commented Sep 11, 2026

Automation disposition: needs-maintainer (reviewed and correct; required checks cannot run on a NOTICE-only diff)

Uh oh!

Vilin97 commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Vilin97 commented Sep 10, 2026 •

edited

Loading

greptile-apps Bot commented Sep 10, 2026 •

edited

Loading