Import the disproof of the Köthe conjecture (Krempa's matrix form) by Vilin97 · Pull Request #408 · LeanPool/lean-pool

Vilin97 · 2026-09-10T19:06:17Z

Summary

Imports tadamcz/koethe — a machine-checked disproof of Köthe's conjecture (1930) in Krempa's matrix form — as LeanPool/Koethe/.

Result. Koethe.KotherConjecture.variants.general_matrix.disproof proves the negation of the research-open statement KotherConjecture.variants.general_matrix of Google DeepMind's Formal Conjectures (FormalConjectures/Wikipedia/Koethe.lean @ 9cbe1d3c, statement and IsNil/KotheRadical copied verbatim, see LeanPool/Koethe/Disproof.lean): there is a ring R with a nil two-sided ideal I such that M_2(I) is not nil. KoetheCounterexample.counterexample gives the witness in every universe. Since each column ideal of M_n(I) is a nil left ideal, this refutes Köthe's original formulation (sum of two nil left ideals is nil); that last step is standard and not formalized, as the README and card state.
Significance. Köthe's conjecture was one of the best-known open problems in noncommutative ring theory for 96 years. The result was announced 2026-09-04/05 (X, then Zulip #AI authored projects > Koethe's Conjecture, where Pace Nielsen — who has worked on the problem — describes it as resolved negatively) and written up as arXiv:2609.07996 (Adamczewski, Böhmler, Marczinzik, 2026-09-07).
Provenance: AI. The Lean proof was written autonomously by a pre-release GPT-6 Astra in Epoch AI's LeanOpenProblems harness (run wikipedia-vega-1000usd, 26 h agent time, $432), verified by Comparator against the Formal Conjectures statement, and packaged by Tom Adamczewski. Upstream commit a94a72aec957cb28d76aa30fb97a01d440990d7f, Apache-2.0 (LICENSE + NOTICE in the repo; the vendored statement is © The Formal Conjectures Authors, Apache-2.0, credited in the module docstring).

Reusable infrastructure

Beyond the headline theorem, the development contains general results with Mathlib vocabulary:

KoetheMultiProjective.exists_common_zero: over an algebraically closed field, at most 2N polynomials multihomogeneous of common positive degree in N blocks of three variables have a common zero with no zero block (Segre cone + Nullstellensatz + Krull height; a multiprojective intersection theorem proved by affine commutative algebra).
KoetheCounterexample.maskMortality / exists_universalMortalSequence: a matrix-mortality theorem for one-row pencils and a diagonal construction of universal mortal letter sequences.
KoetheCounterexample.nil_of_all_pencils_nil: nilness of a three-generator non-unital algebra follows from nilness of its root-row pencils (finite homogeneous-linear systems, resolvent argument).
ShiftWitness.nonnil_matrix_of_fixed_vector / exists_witness_of_nil_subalgebra: from a nil non-unital subalgebra with a transcendental-scalar fixed vector to a nil ideal of its unitization with a non-nilpotent 2 × 2 matrix.

Porting changes (upstream Lean v4.28.0 / Mathlib v4.28.0 → pool toolchain)

Split the single 3,252-line upstream file into 20 modules along its own KoetheProofPartNN boundaries (parts 19+20 merged into Counterexample.lean; the Formal Conjectures statement block in Disproof.lean).
import Mathlib → minimal imports per file (computed with linter.minImports, then pruned against the transitive closure and repaired by building); dropped the 20 set_option autoImplicit false lines. Every file also compiles with -DautoImplicit=false, so no implicit was auto-bound.
API drift: MvPolynomial/AddMonoidAlgebra is now a structure, so balancedPart is defined through AddMonoidAlgebra.coeffLinearEquiv and balancedPart_monomial is proved coefficientwise; Finset.mem_antidiagonal → Finset.HasAntidiagonal.mem_antidiagonal; Ideal.primeHeight_add_one_le_of_lt → Ideal.height_add_one_le_of_lt_of_isPrime; Finsupp.finset_sum_apply/Polynomial.finset_sum_coeff/if_pos/if_neg/dif_pos/Set.setOf_true renames; Fintype sums over structure-field instances (System.add/prepend/atom) go through three small bridging lemmas.
Linter-driven: field Pencil.constant renamed scalar (the quality gate's textual scan for unchecked declarations matches the word constant); FreePos made an abbrev; docstrings added for all definitions and structure fields; two @[simp] attributes dropped (constantWord_degree, specialize_constantWord, not in simp-normal form); letI → let/have per the style linter; three auxiliary lemmas generalized from [Fintype ι] to [Finite ι] (unused-Fintype linter). Removed the unused local notation "Nil*" and two TODO(lezeau) comments inherited from Formal Conjectures.
No theorem statement was weakened. Diff against upstream (headers/imports/docstrings stripped): 223 lines added, 129 removed, all listed above.

Trust and axiom audit

#print axioms on …general_matrix.disproof, KoetheCounterexample.counterexample, exists_common_zero, maskMortality, exists_universalMortalSequence, nil_of_all_pencils_nil: [propext, Classical.choice, Quot.sound]. No sorry/admit/axiom/unsafe/partial/opaque/native_decide, no set_option, no nolint. Structures (Pencil, PeriodicMask, System) carry only data and elementary side conditions (period_pos, nonzero, linear_off_root); no mathematical content is postulated in a field. The statement in Disproof.lean is byte-identical to the Formal Conjectures statement modulo the theorem … : ¬ (∀ …) wrapper.

Local checks

lake build LeanPool.Koethe: warning-free. lake build LeanPool (whole pool root, after the copied cache) warning-free.
lake exe mk_all --check: no update necessary.
lake exe runLinter LeanPool.Koethe: "Linting passed".
lake exe lint-style on all 21 files: clean.
python -m lean_pool.quality --repo ..: run locally on the full pool (results in the review comment).

Compile-time measurements

Clean rebuild of the project only (Mathlib oleans warm), time lake build LeanPool.Koethe after deleting the project's artifacts; WSL2, 32 threads, 45 GB RAM, Lean v4.34.0-rc1.

	wall	user	sys	slowest module	sum of module times
baseline (port with `import Mathlib` everywhere)	33.4 s	68.5 s	32.0 s	`MultiProjective` 5.7 s	≈ 75 s
after import narrowing	19.1 s	36.7 s	14.2 s	`MultiProjective` 3.6 s	≈ 33 s
optimized (imports + two hot spots, current head)	16.3 s	33.8 s	13.8 s	`MultiProjective` 2.7 s	≈ 32 s

Per-declaration heartbeats (-Dlinter.countHeartbeats=true, the pool's /profile method): every named declaration is at most 35 units (ShiftWitness.Endpoint companion-matrix lemmas), far below the default 200 k. The -Dprofiler pass located one hot spot, a 1.0 s refine in MultiProjective; bisection showed it was the untyped tactic have hlt := Ideal.height_add_one_le_of_lt_of_isPrime … in vertexIdeal_height_lower_bound (a have is a refine_lift), and giving the term its expected type cuts that module's tactic execution from 1.5 s to 0.5 s. The anonymous Countable GroundField instance was the largest heartbeat item in CI's first profile (755 units); a named instance with a direct Set.Countable.mono proof measures 2 units. Nothing else is above 0.25 s; the remaining cost is import loading (1.0–1.5 s per module). No heartbeat override was ever needed.

🤖 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>

github-actions · 2026-09-10T19:10:25Z

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 43.65 s (= 0.73 min) — user 73.97 s, sys 18.65 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 2,631 maxHeartbeats units across 21 files (3,535 added LOC).

Sum of lean --profile: 58191.0 ms (= 58.19 s). Import-excluded time: 31018.0 ms (= 31.02 s).

Count-heartbeats wall-clock total: 83.76 s. Repeated import cost inside lean --profile: 27173.0 ms (= 27.17 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	`lean --profile` (s)	Without import (s)	Import (s)	Decls
`LeanPool/Koethe/Counterexample.lean`	69	755	3.03	2.02	0.45	1.57	4
`LeanPool/Koethe/MultiProjective.lean`	807	398	10.51	10.64	9.13	1.51	85
`LeanPool/Koethe/Linearization/Basic.lean`	247	325	3.87	3.02	2.04	0.98	25
`LeanPool/Koethe/ShiftWitness/Endpoint.lean`	187	202	4.68	4.30	2.83	1.47	8
`LeanPool/Koethe/Pencil.lean`	149	153	2.36	1.49	0.51	0.98	18
`LeanPool/Koethe/ShiftWitness/Band.lean`	140	120	5.43	3.36	2.35	1.01	12
`LeanPool/Koethe/Linearization/Pencil.lean`	153	112	3.22	2.27	1.26	1.01	10
`LeanPool/Koethe/Mortality/Homogeneous.lean`	201	99	3.98	2.69	1.18	1.51	21
`LeanPool/Koethe/Mortality/FormalWord.lean`	154	83	4.41	3.28	1.74	1.54	16
`LeanPool/Koethe/Mortality/Degree.lean`	91	68	3.42	1.85	0.68	1.17	4
`LeanPool/Koethe/MaskSequence/Basic.lean`	203	66	3.09	2.87	1.87	1.00	20
`LeanPool/Koethe/Mortality/Mask.lean`	186	54	3.44	2.50	0.97	1.53	18
`LeanPool/Koethe/Mortality/Minors.lean`	191	53	3.80	2.68	1.49	1.19	11
`LeanPool/Koethe/Linearization/Nil.lean`	88	36	3.04	1.39	0.37	1.02	3
`LeanPool/Koethe/MaskSequence/Chain.lean`	111	30	2.80	1.44	0.44	1.00	10
`LeanPool/Koethe/ShiftWitness/Eigenvector.lean`	95	30	4.89	2.54	1.04	1.50	10
`LeanPool/Koethe/MaskSequence/Universal.lean`	101	18	2.98	1.47	0.46	1.01	5
`LeanPool/Koethe/Mortality/MaskMortality.lean`	141	14	3.79	2.28	0.74	1.54	3
`LeanPool/Koethe/ShiftWitness/Witness.lean`	74	12	3.73	2.40	0.90	1.50	4
`LeanPool/Koethe/Disproof.lean`	79	3	3.81	1.92	0.36	1.56	1
`LeanPool/Koethe.lean`	68	0	3.48	1.78	0.21	1.57	0
Total	3,535	2,631	83.76	58.19	31.02	27.17	288

Aggregate phase totals

Phase	Time
`import`	27173.0 ms (= 27.17 s)
`typeclass inference`	8518.8 ms (= 8.52 s)
`interpretation`	5844.0 ms (= 5.84 s)
`tactic execution`	5391.2 ms (= 5.39 s)
`simp`	5326.6 ms (= 5.33 s)
`elaboration`	1678.2 ms (= 1.68 s)
`type checking`	1361.1 ms (= 1.36 s)
`initialization`	675.3 ms (= 0.68 s)
`tacticAnalysis`	616.8 ms (= 0.62 s)
`linting`	325.0 ms (= 0.33 s)
`overlappingInstancesLinter`	243.6 ms (= 0.24 s)
`parsing`	222.1 ms (= 0.22 s)

Slowest changed modules (from `lake build`)

Changed module	Lake time
`LeanPool.Koethe.MultiProjective`	16.00 s
`LeanPool.Koethe.ShiftWitness.Endpoint`	11.00 s
`LeanPool.Koethe.Mortality.Minors`	7.60 s
`LeanPool.Koethe.Pencil`	6.80 s
`LeanPool.Koethe.ShiftWitness.Band`	6.50 s
`LeanPool.Koethe.Linearization.Basic`	5.80 s
`LeanPool.Koethe.ShiftWitness.Eigenvector`	4.60 s
`LeanPool.Koethe.Mortality.Homogeneous`	4.40 s
`LeanPool.Koethe.ShiftWitness.Witness`	4.10 s
`LeanPool.Koethe.Linearization.Pencil`	3.60 s
`LeanPool.Koethe.MaskSequence.Basic`	3.40 s
`LeanPool.Koethe.Mortality.Degree`	3.20 s

Per-file `lean --profile` output

`LeanPool/Koethe.lean`

import took 1.57s
cumulative profiling times:
	elaboration 0.192ms
	import 1.57s
	initialization 29ms
	interpretation 179ms
	linting 0.421ms
	module linting 0.00152ms
	overlappingInstancesLinter 0.926ms
	parsing 0.0871ms
	tacticAnalysis 1.53ms
real 2.42
user 1.37
sys 1.05

`LeanPool/Koethe/Counterexample.lean`

import took 1.57s
cumulative profiling times:
	attribute application 0.209ms
	congr simp thm 0.19ms
	elaboration 25.3ms
	fix level params 0.207ms
	import 1.57s
	initialization 28.9ms
	instantiate metavars 0.0728ms
	interpretation 206ms
	let-to-have transformation 0.0464ms
	linting 2.9ms
	module linting 0.00132ms
	overlappingInstancesLinter 4.77ms
	parsing 2.64ms
	process pre-definitions 1.42ms
	share common exprs 0.611ms
	simp 1.71ms
	tactic execution 7.18ms
	tacticAnalysis 8.21ms
	type checking 14.1ms
	typeclass inference 148ms
real 2.52
user 1.58
sys 1.08

`LeanPool/Koethe/Disproof.lean`

import took 1.56s
cumulative profiling times:
	attribute application 0.027ms
	compilation (IR) 0.0314ms
	compilation (LCNF base) 1.2ms
	compilation (LCNF impure) 0.135ms
	compilation (LCNF mono) 0.262ms
	elaboration 9.69ms
	fix level params 0.243ms
	import 1.56s
	initialization 33.2ms
	instantiate metavars 0.472ms
	interpretation 206ms
	let-to-have transformation 0.0284ms
	linting 2.73ms
	module linting 0.00179ms
	overlappingInstancesLinter 3.95ms
	parsing 2.56ms
	process pre-definitions 1.18ms
	share common exprs 0.494ms
	tactic execution 22.9ms
	tacticAnalysis 7.99ms
	type checking 8.37ms
	typeclass inference 58ms
real 2.50
user 1.45
sys 1.11

`LeanPool/Koethe/Linearization/Basic.lean`

import took 980ms
simp took 112ms
cumulative profiling times:
	attribute application 2.46ms
	blocked (unaccounted) 155ms
	compilation (IR) 0.834ms
	compilation (LCNF base) 11.3ms
	compilation (LCNF impure) 4.72ms
	compilation (LCNF mono) 12.6ms
	congr simp thm 8.11ms
	elaboration 133ms
	fix level params 2.45ms
	import 980ms
	initialization 42ms
	instantiate metavars 1.72ms
	interpretation 302ms
	let-to-have transformation 0.274ms
	linting 23ms
	module linting 0.00176ms
	overlappingInstancesLinter 19.5ms
	parsing 16.4ms
	process pre-definitions 9.45ms
	share common exprs 5.72ms
	simp 514ms
	tactic execution 158ms
	tacticAnalysis 44.3ms
	type checking 74.9ms
	typeclass inference 499ms
real 2.50
user 2.70
sys 0.80

`LeanPool/Koethe/Linearization/Nil.lean`

import took 1.02s
cumulative profiling times:
	attribute application 0.0517ms
	congr simp thm 0.215ms
	elaboration 15.6ms
	fix level params 0.399ms
	import 1.02s
	initialization 30.2ms
	instantiate metavars 0.375ms
	interpretation 180ms
	let-to-have transformation 0.059ms
	linting 7.19ms
	module linting 0.00125ms
	overlappingInstancesLinter 8.17ms
	parsing 3.33ms
	process pre-definitions 1.44ms
	share common exprs 0.807ms
	simp 1.49ms
	tactic execution 43.8ms
	tacticAnalysis 9.58ms
	type checking 11.5ms
	typeclass inference 59.6ms
real 1.87
user 1.18
sys 0.81

`LeanPool/Koethe/Linearization/Pencil.lean`

import took 1.01s
cumulative profiling times:
	attribute application 0.5ms
	compilation (IR) 0.298ms
	compilation (LCNF base) 3.08ms
	compilation (LCNF impure) 1.9ms
	compilation (LCNF mono) 2.85ms
	congr simp thm 5.41ms
	elaboration 73.7ms
	fix level params 1.93ms
	import 1.01s
	initialization 34.9ms
	instantiate metavars 1.88ms
	interpretation 217ms
	let-to-have transformation 0.151ms
	linting 12.6ms
	module linting 0.00154ms
	overlappingInstancesLinter 12.4ms
	parsing 8.51ms
	process pre-definitions 9.25ms
	share common exprs 4.44ms
	simp 377ms
	tactic execution 134ms
	tacticAnalysis 24.8ms
	type checking 44.7ms
	typeclass inference 285ms
real 2.30
user 2.07
sys 0.83

`LeanPool/Koethe/MaskSequence/Basic.lean`

import took 999ms
cumulative profiling times:
	attribute application 1.52ms
	blocked (unaccounted) 1.22ms
	compilation (IR) 0.143ms
	compilation (LCNF base) 1.53ms
	compilation (LCNF impure) 0.78ms
	compilation (LCNF mono) 1.39ms
	congr simp thm 10.4ms
	elaboration 82.2ms
	fix level params 1.85ms
	import 999ms
	initialization 28.7ms
	instantiate metavars 1.33ms
	interpretation 426ms
	let-to-have transformation 0.24ms
	linting 19.1ms
	module linting 0.00155ms
	norm_num 4.55ms
	overlappingInstancesLinter 16.9ms
	parsing 14.3ms
	process pre-definitions 12.3ms
	ring 20.7ms
	share common exprs 6.93ms
	simp 336ms
	tactic execution 133ms
	tacticAnalysis 36.3ms
	type checking 69.4ms
	typeclass inference 641ms
real 2.28
user 2.64
sys 0.81

`LeanPool/Koethe/MaskSequence/Chain.lean`

import took 1s
cumulative profiling times:
	attribute application 0.153ms
	congr simp thm 0.305ms
	elaboration 49.6ms
	fix level params 0.578ms
	import 1s
	initialization 34.3ms
	instantiate metavars 0.547ms
	interpretation 209ms
	let-to-have transformation 0.127ms
	linting 9.46ms
	module linting 0.00171ms
	overlappingInstancesLinter 11.3ms
	parsing 7.57ms
	process pre-definitions 6.8ms
	share common exprs 1.42ms
	simp 2.08ms
	tactic execution 36.5ms
	tacticAnalysis 23.1ms
	type checking 11.9ms
	typeclass inference 32.4ms
real 1.87
user 1.21
sys 0.82

`LeanPool/Koethe/MaskSequence/Universal.lean`

import took 1.01s
cumulative profiling times:
	attribute application 0.0587ms
	congr simp thm 0.927ms
	elaboration 22.9ms
	fix level params 0.707ms
	import 1.01s
	initialization 28.8ms
	instantiate metavars 0.551ms
	interpretation 195ms
	let-to-have transformation 0.0828ms
	linting 7.35ms
	module linting 0.00126ms
	overlappingInstancesLinter 6.02ms
	parsing 6.99ms
	process pre-definitions 2.28ms
	share common exprs 1.65ms
	simp 27ms
	tactic execution 72.8ms
	tacticAnalysis 18.4ms
	type checking 29.4ms
	typeclass inference 40.9ms
real 1.84
user 1.24
sys 0.82

`LeanPool/Koethe/Mortality/Degree.lean`

import took 1.17s
cumulative profiling times:
	attribute application 0.0447ms
	congr simp thm 2.73ms
	elaboration 26.5ms
	fix level params 0.732ms
	import 1.17s
	initialization 29.1ms
	instantiate metavars 0.631ms
	interpretation 203ms
	let-to-have transformation 0.0807ms
	linting 6.25ms
	module linting 0.00158ms
	overlappingInstancesLinter 6.33ms
	parsing 4.81ms
	process pre-definitions 2.26ms
	share common exprs 2.13ms
	simp 65.8ms
	tactic execution 55.2ms
	tacticAnalysis 15.5ms
	type checking 27.7ms
	typeclass inference 227ms
real 2.22
user 1.55
sys 0.90

`LeanPool/Koethe/Mortality/FormalWord.lean`

import took 1.54s
simp took 314ms
simp took 311ms
cumulative profiling times:
	attribute application 1.78ms
	compilation (IR) 0.158ms
	compilation (LCNF base) 2.27ms
	compilation (LCNF impure) 0.981ms
	compilation (LCNF mono) 1.35ms
	congr simp thm 4.01ms
	elaboration 91.8ms
	fix level params 1.37ms
	import 1.54s
	initialization 29.1ms
	instantiate metavars 1.59ms
	interpretation 276ms
	let-to-have transformation 0.212ms
	linting 12.4ms
	module linting 0.00126ms
	overlappingInstancesLinter 8.42ms
	parsing 10.7ms
	process pre-definitions 6.14ms
	share common exprs 3.89ms
	simp 650ms
	tactic execution 143ms
	tacticAnalysis 30ms
	type checking 64.2ms
	typeclass inference 397ms
real 3.45
user 2.89
sys 1.04

`LeanPool/Koethe/Mortality/Homogeneous.lean`

import took 1.51s
cumulative profiling times:
	attribute application 0.964ms
	compilation (IR) 0.094ms
	compilation (LCNF base) 0.639ms
	compilation (LCNF impure) 0.318ms
	compilation (LCNF mono) 0.514ms
	congr simp thm 4.27ms
	elaboration 81ms
	fix level params 1.81ms
	import 1.51s
	initialization 29.5ms
	instantiate metavars 1.55ms
	interpretation 344ms
	let-to-have transformation 0.334ms
	linting 20.1ms
	module linting 0.00126ms
	overlappingInstancesLinter 16.6ms
	parsing 13.5ms
	process pre-definitions 7.36ms
	share common exprs 5.01ms
	simp 117ms
	tactic execution 138ms
	tacticAnalysis 41.2ms
	type checking 60.1ms
	typeclass inference 298ms
real 2.64
user 2.25
sys 1.05

`LeanPool/Koethe/Mortality/Mask.lean`

import took 1.53s
cumulative profiling times:
	attribute application 0.804ms
	blocked (unaccounted) 3.03ms
	compilation (IR) 0.17ms
	compilation (LCNF base) 1.33ms
	compilation (LCNF impure) 0.942ms
	compilation (LCNF mono) 1.5ms
	congr simp thm 5.35ms
	elaboration 57.5ms
	fix level params 1.48ms
	import 1.53s
	initialization 35.3ms
	instantiate metavars 1.43ms
	interpretation 295ms
	let-to-have transformation 0.176ms
	linting 16.3ms
	module linting 0.00143ms
	overlappingInstancesLinter 13.3ms
	parsing 11.4ms
	process pre-definitions 5.94ms
	share common exprs 3.46ms
	simp 100ms
	tactic execution 119ms
	tacticAnalysis 37.4ms
	type checking 42.8ms
	typeclass inference 221ms
real 2.59
user 2.02
sys 1.09

`LeanPool/Koethe/Mortality/MaskMortality.lean`

import took 1.54s
cumulative profiling times:
	attribute application 0.0343ms
	congr simp thm 2.72ms
	dsimp 1.73ms
	elaboration 24.7ms
	fix level params 1.12ms
	import 1.54s
	initialization 36.2ms
	instantiate metavars 1.12ms
	interpretation 248ms
	let-to-have transformation 0.0716ms
	linting 12ms
	module linting 0.00158ms
	norm_num 0.54ms
	overlappingInstancesLinter 5.47ms
	parsing 6.83ms
	process pre-definitions 3.62ms
	ring 5.87ms
	share common exprs 2.73ms
	simp 58ms
	tactic execution 116ms
	tacticAnalysis 20.1ms
	type checking 63.2ms
	typeclass inference 134ms
real 2.65
user 1.84
sys 1.08

`LeanPool/Koethe/Mortality/Minors.lean`

import took 1.19s
cumulative profiling times:
	attribute application 0.124ms
	congr simp thm 4.96ms
	elaboration 56.1ms
	fix level params 1.88ms
	import 1.19s
	initialization 39.8ms
	instantiate metavars 2.51ms
	interpretation 273ms
	let-to-have transformation 0.172ms
	linting 20.1ms
	module linting 0.00146ms
	overlappingInstancesLinter 13.7ms
	parsing 12.4ms
	process pre-definitions 6.91ms
	share common exprs 4.92ms
	simp 129ms
	tactic execution 244ms
	tacticAnalysis 36.8ms
	type checking 54.6ms
	typeclass inference 593ms
real 2.54
user 2.36
sys 0.93

`LeanPool/Koethe/MultiProjective.lean`

import took 1.51s
tactic execution of Lean.Parser.Tactic.refine took 2.55s
tactic execution of Lean.Parser.Tactic.refine took 133ms
cumulative profiling times:
	attribute application 17.6ms
	blocked (unaccounted) 43.5ms
	compilation (IR) 0.259ms
	compilation (LCNF base) 3.19ms
	compilation (LCNF impure) 1.46ms
	compilation (LCNF mono) 2.37ms
	congr simp thm 19.6ms
	elaboration 557ms
	fix level params 9.48ms
	import 1.51s
	initialization 29.2ms
	instantiate metavars 9.87ms
	interpretation 845ms
	let-to-have transformation 1.68ms
	linting 96.2ms
	module linting 0.00137ms
	overlappingInstancesLinter 49.8ms
	parsing 58.8ms
	process pre-definitions 45.3ms
	share common exprs 28.7ms
	simp 990ms
	tactic execution 3.43s
	tacticAnalysis 147ms
	type checking 401ms
	typeclass inference 2.34s
real 6.53
user 10.04
sys 1.12

`LeanPool/Koethe/Pencil.lean`

import took 984ms
cumulative profiling times:
	attribute application 2.4ms
	blocked (unaccounted) 17.4ms
	compilation (IR) 0.0658ms
	compilation (LCNF base) 0.585ms
	compilation (LCNF impure) 0.366ms
	compilation (LCNF mono) 0.731ms
	congr simp thm 4.03ms
	elaboration 74.5ms
	fix level params 0.491ms
	import 984ms
	initialization 29.5ms
	instantiate metavars 0.332ms
	interpretation 214ms
	let-to-have transformation 0.126ms
	linting 9.64ms
	module linting 0.0013ms
	overlappingInstancesLinter 9.66ms
	parsing 9.42ms
	process pre-definitions 4.83ms
	share common exprs 1.17ms
	simp 7.2ms
	tactic execution 17.6ms
	tacticAnalysis 21.5ms
	type checking 22.8ms
	typeclass inference 56.9ms
real 1.91
user 1.29
sys 0.80

`LeanPool/Koethe/ShiftWitness/Band.lean`

import took 1.01s
simp took 169ms
simp took 301ms
simp took 231ms
simp took 152ms
cumulative profiling times:
	attribute application 1.7ms
	compilation (IR) 0.097ms
	compilation (LCNF base) 3.22ms
	compilation (LCNF impure) 0.575ms
	compilation (LCNF mono) 2.17ms
	congr simp thm 10.8ms
	elaboration 105ms
	fix level params 4.82ms
	import 1.01s
	initialization 29.8ms
	instantiate metavars 3.43ms
	interpretation 230ms
	let-to-have transformation 0.48ms
	linting 14.6ms
	module linting 0.00122ms
	overlappingInstancesLinter 12.5ms
	parsing 9.36ms
	process pre-definitions 12.6ms
	share common exprs 10.2ms
	simp 1.21s
	tactic execution 96.1ms
	tacticAnalysis 29.3ms
	type checking 111ms
	typeclass inference 452ms
real 3.03
user 3.11
sys 0.84

`LeanPool/Koethe/ShiftWitness/Eigenvector.lean`

import took 1.5s
cumulative profiling times:
	attribute application 0.322ms
	congr simp thm 1.72ms
	elaboration 58.5ms
	fix level params 1.42ms
	import 1.5s
	initialization 39.5ms
	instantiate metavars 2.09ms
	interpretation 252ms
	let-to-have transformation 0.165ms
	linting 8.58ms
	module linting 0.00126ms
	norm_num 0.335ms
	overlappingInstancesLinter 8.67ms
	parsing 5.94ms
	process pre-definitions 5.62ms
	ring 7.55ms
	share common exprs 3.4ms
	simp 139ms
	tactic execution 53.9ms
	tacticAnalysis 19.2ms
	type checking 38.6ms
	typeclass inference 396ms
real 2.67
user 2.14
sys 1.03

`LeanPool/Koethe/ShiftWitness/Endpoint.lean`

import took 1.47s
simp took 121ms
simp took 139ms
cumulative profiling times:
	attribute application 10.3ms
	compilation (IR) 0.0985ms
	compilation (LCNF base) 4.9ms
	compilation (LCNF impure) 0.493ms
	compilation (LCNF mono) 1.29ms
	congr simp thm 7.54ms
	elaboration 103ms
	fix level params 3.72ms
	import 1.47s
	initialization 29.1ms
	instantiate metavars 5.84ms
	interpretation 342ms
	let-to-have transformation 0.316ms
	linting 19.7ms
	module linting 0.00124ms
	overlappingInstancesLinter 10.2ms
	parsing 13.1ms
	process pre-definitions 16ms
	share common exprs 8.38ms
	simp 589ms
	tactic execution 285ms
	tacticAnalysis 34ms
	type checking 143ms
	typeclass inference 1.2s
real 3.66
user 3.92
sys 1.03

`LeanPool/Koethe/ShiftWitness/Witness.lean`

import took 1.5s
cumulative profiling times:
	attribute application 0.346ms
	congr simp thm 0.571ms
	elaboration 30.4ms
	fix level params 0.744ms
	import 1.5s
	initialization 29.2ms
	instantiate metavars 0.0901ms
	interpretation 202ms
	let-to-have transformation 0.18ms
	linting 4.4ms
	module linting 0.00163ms
	overlappingInstancesLinter 5.01ms
	parsing 3.44ms
	process pre-definitions 5.49ms
	share common exprs 1.32ms
	simp 12.3ms
	tactic execution 85.2ms
	tacticAnalysis 10.6ms
	type checking 67.8ms
	typeclass inference 440ms
real 2.78
user 1.99
sys 1.07

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

… 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>

greptile-apps · 2026-09-10T19:12:43Z

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

Adds the counterexample and its Formal Conjectures-facing disproof theorem.
Adds supporting multiprojective, mortality, sequence, linearization, and shift-witness modules.
Registers the project and exposes it through the project and repository umbrella imports.

_{Reviews (3) · Last reviewed commit: "Merge branch 'main' into claude/daily-im..."}

Give the two height-step terms in MultiProjective their expected type, which cuts that module's tactic execution from 1.5 s to 0.5 s (the untyped `have` spent ~1 s elaborating `Ideal.height_add_one_le_of_lt_of_isPrime`), and name the countable ground-field instance with a direct proof (its countHeartbeats figure drops from 749 to 2 units). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Vilin97 · 2026-09-10T21:42:23Z

Automated review — approve

Reviewed exact head 05960c8aaf9034ae00d3ec97f157f9dd85ba2209.

Faithfulness. The headline

theorem Koethe.KotherConjecture.variants.general_matrix.disproof :
    ¬ (∀ {R : Type*} [Ring R] {I : TwoSidedIdeal R},
      IsNil I → ∀ (n : Type*) [Fintype n], IsNil (matrix n I))

is the negation of KotherConjecture.variants.general_matrix in FormalConjectures/Wikipedia/Koethe.lean at 9cbe1d3c; I diffed the two files: IsNil, KotheRadical, the open scoped Classical in, binder types and conclusion are identical. TwoSidedIdeal.matrix is Mathlib's entrywise M_n(I) (mem_matrix : M ∈ I.matrix n ↔ ∀ i j, M i j ∈ I). The statement is universe-polymorphic in R and n, and KoetheCounterexample.counterexample supplies a witness in every universe (AlgebraicClosure (ULift (ZMod 2)), index ULift (Fin 2)), so the ¬∀ is discharged without any universe trick. The three structures (Pencil, PeriodicMask, System) carry data and elementary side conditions (linear_off_root, period_pos, nonzero) only; no mathematical content is postulated in a field. The card, module docstring and PR scope the result honestly as Krempa's matrix form and state that the reduction from Köthe's original formulation is standard and not formalized.

Trust. Local build in a clean worktree at this head (2,741 jobs) and #print axioms on the headline, counterexample, exists_common_zero, maskMortality, exists_universalMortalSequence, nil_of_all_pencils_nil: [propext, Classical.choice, Quot.sound]. CI's full-pool build, linters, style lint and quality checker (including the environment backdoor audit) are green.

Significance, novelty, sources. A disproof of a named conjecture open since 1930, in the exact form Formal Conjectures registers as research-open; research level by any standard. No Mathlib declaration and no pooled project touches it (the pool's only "Köthe" hits are Köthe sequence spaces in OSforGFF). arXiv:2609.07996 (Adamczewski, Böhmler, Marczinzik, 2026-09-07) exists with the stated title and authors; upstream tadamcz/koethe@a94a72a is Apache-2.0 with a NOTICE whose attribution is carried by #409; provenance: AI is declared and matches the upstream README.

Quality and cost. 20 modules / 3,628 lines with minimal imports, no set_option, docstrings throughout; 44 s changed-module build, 2,631 maxHB, no declaration above 35 units.

No findings. Disposition: merge (squash, after the branch is refreshed for the strict up-to-date rule).

Vilin97 and others added 2 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>

Vilin97 mentioned this pull request Sep 10, 2026

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

Merged

Merge branch 'main' into claude/daily-import-koethe-2026-09-10

ad9a36b

Vilin97 merged commit 8fdcf5a into main Sep 10, 2026
13 checks passed

Vilin97 mentioned this pull request Sep 10, 2026

Formalization imported into Lean Pool tadamcz/koethe#2

Open

Conversation

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

Uh oh!

Summary

Reusable infrastructure

Porting changes (upstream Lean v4.28.0 / Mathlib v4.28.0 → pool toolchain)

Trust and axiom audit

Local checks

Compile-time measurements

Uh oh!

github-actions Bot commented Sep 10, 2026

Proof profile (new / modified Lean files)

Aggregate phase totals

Slowest changed modules (from lake build)

LeanPool/Koethe.lean

LeanPool/Koethe/Counterexample.lean

LeanPool/Koethe/Disproof.lean

LeanPool/Koethe/Linearization/Basic.lean

LeanPool/Koethe/Linearization/Nil.lean

LeanPool/Koethe/Linearization/Pencil.lean

LeanPool/Koethe/MaskSequence/Basic.lean

LeanPool/Koethe/MaskSequence/Chain.lean

LeanPool/Koethe/MaskSequence/Universal.lean

LeanPool/Koethe/Mortality/Degree.lean

LeanPool/Koethe/Mortality/FormalWord.lean

LeanPool/Koethe/Mortality/Homogeneous.lean

LeanPool/Koethe/Mortality/Mask.lean

LeanPool/Koethe/Mortality/MaskMortality.lean

LeanPool/Koethe/Mortality/Minors.lean

LeanPool/Koethe/MultiProjective.lean

LeanPool/Koethe/Pencil.lean

LeanPool/Koethe/ShiftWitness/Band.lean

LeanPool/Koethe/ShiftWitness/Eigenvector.lean

LeanPool/Koethe/ShiftWitness/Endpoint.lean

LeanPool/Koethe/ShiftWitness/Witness.lean

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!

Vilin97 commented Sep 10, 2026

Automated review — approve

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Vilin97 commented Sep 10, 2026 •

edited

Loading

Slowest changed modules (from `lake build`)

`LeanPool/Koethe.lean`

`LeanPool/Koethe/Counterexample.lean`

`LeanPool/Koethe/Disproof.lean`

`LeanPool/Koethe/Linearization/Basic.lean`

`LeanPool/Koethe/Linearization/Nil.lean`

`LeanPool/Koethe/Linearization/Pencil.lean`

`LeanPool/Koethe/MaskSequence/Basic.lean`

`LeanPool/Koethe/MaskSequence/Chain.lean`

`LeanPool/Koethe/MaskSequence/Universal.lean`

`LeanPool/Koethe/Mortality/Degree.lean`

`LeanPool/Koethe/Mortality/FormalWord.lean`

`LeanPool/Koethe/Mortality/Homogeneous.lean`

`LeanPool/Koethe/Mortality/Mask.lean`

`LeanPool/Koethe/Mortality/MaskMortality.lean`

`LeanPool/Koethe/Mortality/Minors.lean`

`LeanPool/Koethe/MultiProjective.lean`

`LeanPool/Koethe/Pencil.lean`

`LeanPool/Koethe/ShiftWitness/Band.lean`

`LeanPool/Koethe/ShiftWitness/Eigenvector.lean`

`LeanPool/Koethe/ShiftWitness/Endpoint.lean`

`LeanPool/Koethe/ShiftWitness/Witness.lean`

greptile-apps Bot commented Sep 10, 2026 •

edited

Loading