Import OpenAI infinite Connes rigidity formalization by Vilin97 · Pull Request #393 · Vilin97/lean-pool

Vilin97 · 2026-09-04T12:28:37Z

Summary

This imports the exact OpenAI Ten Proofs infinite Connes-rigidity endpoint as an
independent Lean Pool project:

ConnesRigidity.exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors

It proves unconditionally that there are a finitely generated property-(T) ICC
group and an infinite family of finitely generated property-(T) ICC groups,
pairwise nonisomorphic and all nonisomorphic to the distinguished group, whose
tracial group von Neumann algebras are nevertheless normally star-isomorphic.

The proof is split into five focused modules plus a small entry module. Every
implementation-only declaration is explicitly private; the 690 declarations in
the cross-module/public dependency surface are documented and audited. The short
ConnesRigidity.infiniteConnesRigidity abbreviation is the generated-card anchor
because the repository's generated-card/style invariant cannot accommodate the
canonical 102-character declaration name on its declaration line. The exact
canonical theorem remains public and is registered in main_results.

Provenance

Canonical OpenAI source: openai/ten-proofs@94bc0fe, Apache-2.0.
Optimization baseline: deancureton/ten-proofs@30c21d7, including Dean Cureton's common-projection factoring.
Further porting, dependency-closure reduction, module/API design, import narrowing, warning repair, and proof optimization in this PR.

Accordingly the project is registered with provenance: mix, crediting OpenAI
and Dean Cureton while retaining the canonical OpenAI commit in source metadata.

Existing pooled project and reuse experiment

This does not replace LeanPool.ConnesRigidity. The existing project's
headline Connes.theoremA is a conditional two-group result: it assumes
property (T) for a particular elementary group and obtains two property-(T) ICC
groups with isomorphic factors. The new endpoint is unconditional, gives a
distinguished group plus an infinite pairwise-nonisomorphic family, and also
records finite generation and all pairwise factor isomorphisms.

I inventoried 265 common declaration base names and tested direct imports and
definitional compatibility. The following foundational pieces are compatible:

CountableDiscreteGroup
same-universe HasKazhdanPropertyT
GroupL2
l2Reindex
leftRegularRepresentation

The proof's key semantic interfaces are not definitionally compatible, already
at IsICC and IsProjectionSupremum (and hence the factor layer). Importing the
existing project merely to reuse the compatible prefix would pull in its entire
23.7k-line dependency, measured locally at 173.17 s and 4.73 GB RSS, while the
adapters needed above the divergence would change the exact endpoint vocabulary
and retain most duplicate proof machinery. The final project therefore remains
independent: this is materially smaller and avoids fragile namespace/import
coupling. A mixed import of both projects was compiled successfully.

Reduction and optimization

Removed 262 declarations outside the transitive source/kernel dependency
closure of the endpoint.
Narrowed every Mathlib import; 87 focused imports remain across the five leaf
modules. In particular, the import-shaker false positive
Mathlib.NumberTheory.SelbergSieve is absent.
Replaced the expensive boxDetectionSet Pi-of-subtype index/cast layer with a
shared-bound subtype, eliminating repeated dependent casts.
Removed dead aliases and unused arguments/instances, deduplicated local
infrastructure, repaired current-Mathlib proof regressions, and made the API
surface explicit.
Reduced all proof bodies below 200 lines; the maximum is 135 lines across
1,713 measured theorem/lemma blocks.
All five implementation files are below 10,000 physical lines.

Baseline	Non-comment/source code lines	Delta to PR
OpenAI canonical	33,385	-554 (-1.66%)
Dean optimized fork	33,746	-915 (-2.71%)
This PR	32,831	—

The checked-in physical total is 40,573 lines because the split adds headers,
module documentation, imports, public API documentation, and explicit
private/public audit markers. Lean Pool's quality-code count is 33,671;
32,831 is the like-for-like substantive source count excluding those structural
lines.

Module	Physical lines	Quality code lines	Max proof lines
`UniversalLattice`	9,071	7,607	119
`CarryAndCrossedProduct`	8,582	6,946	135
`SpectralAndPropertyT`	8,844	7,485	120
`GroupConstruction`	8,681	7,263	78
`FactorAndRigidity`	5,375	4,368	121

The unported Dean monolith on this repository's current Mathlib took 336.18 s,
11.00 GB RSS, and ended with 69 errors plus 267 warnings. A final forced module
validation of the port took 29 s, 31 s, 25 s, 16 s, and 17 s respectively
(118 s summed); the full dependency chain peaked at 2.38 GB RSS. All final
builds are warning-free.

Verification

lake build LeanPool.InfiniteConnesRigidity (all leaf modules rebuilt; clean)
lake exe runLinter LeanPool.InfiniteConnesRigidity (0 findings)
lake exe lint-style LeanPool.InfiniteConnesRigidity (clean)
lake exe mk_all --check (No update necessary)
generated project-card check (current)
focused quality option/backdoor audit (clean)
forbidden construct/import scan (no sorry, admit, unsafe, partial,
axiom, opaque, gate-changing set_option, broad Mathlib, or Selberg
sieve import)
quality declaration parser: 690 public declarations, zero unqualified leaks;
all 690 passed the environment/axiom audit
exact endpoint and card alias both depend only on propext,
Classical.choice, and Quot.sound
exact endpoint signature printed and compared after the final build
mixed integration module importing both LeanPool.ConnesRigidity and
LeanPool.InfiniteConnesRigidity compiled successfully
git diff --check and content-only path audit passed

The static repository-wide quality pass had only the expected generic blank
declaration-check entries for unrelated projects whose oleans were not present
in this focused worktree; filtering showed no InfiniteConnesRigidity finding.
CI remains authoritative for the fully cached umbrella run.

greptile-apps · 2026-09-04T12:30:32Z

Greptile Summary

The PR adds an independently packaged formalization of the unconditional infinite Connes-rigidity result.

Introduces five implementation modules and a small public entry module.
Registers both the canonical theorem and its shorter catalog alias.
Connects the project to the umbrella import and project registry.

Important Files Changed

Filename	Overview
LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean	Defines the canonical unconditional infinite-family theorem and its registry-friendly alias; no accepted blocking issue was identified.
LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean	Supplies spectral and property-(T) infrastructure used by the headline construction; no accepted blocking issue was identified.
LeanPool/InfiniteConnesRigidity/GroupConstruction.lean	Implements the group-family construction consumed by the rigidity endpoint; no accepted blocking issue was identified.
LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean	Adds carry-group, duality, and crossed-product infrastructure; no accepted blocking issue was identified.
LeanPool/InfiniteConnesRigidity/UniversalLattice.lean	Provides the foundational universal-lattice vocabulary and results for the new project; no accepted blocking issue was identified.
LeanPool/InfiniteConnesRigidity.lean	Exposes the project through the final rigidity module and documents its public entry point.
LeanPool/projects.yml	Registers the new project, source metadata, and two resolvable public main results.
LeanPool.lean	Adds the new project modules to the umbrella import graph.

_{Reviews (7): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

github-actions · 2026-09-04T12:42:57Z

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 274.70 s (= 4.58 min) — user 642.52 s, sys 10.07 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: 30,695 maxHeartbeats units across 6 files (40,573 added LOC).

Sum of lean --profile: 621529.5 ms (= 621.53 s). Import-excluded time: 611969.5 ms (= 611.97 s).

Count-heartbeats wall-clock total: 548.64 s. Repeated import cost inside lean --profile: 9560.0 ms (= 9.56 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/InfiniteConnesRigidity/SpectralAndPropertyT.lean`	8,844	9,506	96.62	116.72	115.35	1.37	416
`LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean`	8,582	9,187	171.46	141.95	140.60	1.35	612
`LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean`	5,375	6,669	99.15	92.13	90.72	1.41	362
`LeanPool/InfiniteConnesRigidity/UniversalLattice.lean`	9,071	2,699	101.49	150.72	149.46	1.26	539
`LeanPool/InfiniteConnesRigidity/GroupConstruction.lean`	8,681	2,634	77.32	117.04	115.59	1.45	497
`LeanPool/InfiniteConnesRigidity.lean`	20	0	2.60	2.96	0.24	2.72	0
Total	40,573	30,695	548.64	621.53	611.97	9.56	2426

Aggregate phase totals

Phase	Time
`typeclass inference`	273500.0 ms (= 273.50 s)
`tactic execution`	104100.0 ms (= 104.10 s)
`simp`	75710.0 ms (= 75.71 s)
`interpretation`	40864.0 ms (= 40.86 s)
`type checking`	32320.0 ms (= 32.32 s)
`blocked (unaccounted)`	30060.0 ms (= 30.06 s)
`elaboration`	26180.1 ms (= 26.18 s)
`import`	9560.0 ms (= 9.56 s)
`tacticAnalysis`	6251.9 ms (= 6.25 s)
`process pre-definitions`	4465.0 ms (= 4.46 s)
`linting`	4021.3 ms (= 4.02 s)
`parsing`	2763.0 ms (= 2.76 s)

Slowest changed modules (from `lake build`)

Changed module	Lake time
`LeanPool.InfiniteConnesRigidity.UniversalLattice`	73.00 s
`LeanPool.InfiniteConnesRigidity.CarryAndCrossedProduct`	66.00 s
`LeanPool.InfiniteConnesRigidity.SpectralAndPropertyT`	51.00 s
`LeanPool.InfiniteConnesRigidity.FactorAndRigidity`	38.00 s
`LeanPool.InfiniteConnesRigidity.GroupConstruction`	36.00 s
`LeanPool.InfiniteConnesRigidity`	1.50 s

Per-file `lean --profile` output

`LeanPool/InfiniteConnesRigidity.lean`

import took 2.72s
cumulative profiling times:
	elaboration 0.124ms
	import 2.72s
	initialization 38.5ms
	interpretation 204ms
	linting 0.271ms
	module linting 0.00127ms
	overlappingInstancesLinter 0.357ms
	parsing 0.0278ms
	tacticAnalysis 0.864ms
real 3.57
user 1.36
sys 1.15

`LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean`

import took 1.35s
tactic execution of Lean.Parser.Tactic.change took 121ms
tactic execution of Lean.Parser.Tactic.change took 5.31s
typeclass inference of Nonempty took 170ms
typeclass inference of Nonempty took 166ms
tactic execution of Lean.Parser.Tactic.decide took 284ms
simp took 2.1s
typeclass inference of ZeroHomClass took 317ms
typeclass inference of AddZero took 291ms
typeclass inference of ZeroHomClass took 247ms
typeclass inference of AddGroup took 398ms
typeclass inference of AddGroup took 188ms
typeclass inference of ZeroHomClass took 275ms
typeclass inference of AddHomClass took 369ms
typeclass inference of ZeroHomClass took 254ms
typeclass inference of AddZero took 267ms
typeclass inference of AddZeroClass took 427ms
typeclass inference of AddZeroClass took 248ms
typeclass inference of AddCommGroup took 467ms
typeclass inference of AddGroup took 608ms
typeclass inference of AddGroup took 294ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 185ms
typeclass inference of AddZeroClass took 673ms
typeclass inference of AddZeroClass took 281ms
typeclass inference of AddZeroClass took 660ms
typeclass inference of AddZeroClass took 385ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 114ms
typeclass inference of MulOne took 293ms
typeclass inference of AddZeroClass took 417ms
typeclass inference of AddZeroClass took 242ms
typeclass inference of MulOneClass took 428ms
typeclass inference of MulOneClass took 254ms
typeclass inference of AddZeroClass took 461ms
typeclass inference of AddZeroClass took 271ms
typeclass inference of MulOne took 263ms
typeclass inference of Group took 396ms
typeclass inference of Group took 193ms
elaboration took 2.88s
typeclass inference of Group took 201ms
typeclass inference of Monoid took 261ms
typeclass inference of AddCommGroup took 492ms
typeclass inference of AddCommGroup took 504ms
typeclass inference of CommRing took 140ms
typeclass inference of Semiring took 321ms
typeclass inference of Module.Projective took 443ms
typeclass inference of ZeroHomClass took 427ms
typeclass inference of ZeroHomClass took 412ms
typeclass inference of AddCommGroup took 525ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 115ms
type checking took 145ms
typeclass inference of One took 363ms
typeclass inference of One took 381ms
typeclass inference of One took 361ms
typeclass inference of One took 382ms
typeclass inference of Mul took 454ms
typeclass inference of Mul took 476ms
typeclass inference of AddZeroClass took 433ms
typeclass inference of AddZeroClass took 258ms
typeclass inference of Group took 408ms
typeclass inference of Group took 190ms
typeclass inference of Group took 186ms
typeclass inference of MulOne took 253ms
typeclass inference of Group took 186ms
typeclass inference of Group took 190ms
typeclass inference of Group took 188ms
typeclass inference of Group took 413ms
typeclass inference of Group took 196ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 227ms
tactic execution of Lean.Parser.Tactic.exact took 7.5s
tactic execution of Lean.Parser.Tactic.exact took 7.19s
typeclass inference of ZeroHomClass took 116ms
tactic execution of Lean.Parser.Tactic.obtain took 753ms
type checking took 108ms
typeclass inference of AddCommMonoid took 122ms
typeclass inference of AddCommMonoid took 124ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 457ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 286ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 282ms
tactic execution of Lean.Parser.Tactic.refine took 129ms
typeclass inference of CoeT took 174ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 138ms
interpretation of Mathlib.Tactic.FieldSimp._aux_Mathlib_Tactic_FieldSimp___elabRules_Mathlib_Tactic_FieldSimp_fieldSimp_1._boxed took 126ms
cumulative profiling times:
	attribute application 187ms
	blocked (unaccounted) 7.54s
	compilation (IR) 1.83ms
	compilation (LCNF base) 38.1ms
	compilation (LCNF impure) 7.91ms
	compilation (LCNF mono) 25.7ms
	congr simp thm 182ms
	dsimp 342ms
	elaboration 7.62s
	fix level params 78.2ms
	import 1.35s
	initialization 28.6ms
	instantiate metavars 100ms
	interpretation 7.77s
	let-to-have transformation 104ms
	linting 728ms
	module linting 0.00134ms
	norm_num 174ms
	overlappingInstancesLinter 188ms
	parsing 580ms
	process pre-definitions 1.06s
	ring 154ms
	share common exprs 385ms
	simp 7.99s
	tactic execution 34.3s
	tacticAnalysis 1.16s
	type checking 7.76s
	typeclass inference 62.1s
real 71.96
user 134.04
sys 1.55

`LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean`

import took 1.41s
simp took 968ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 201ms
typeclass inference of MeasureTheory.IsFiniteMeasureOnCompacts took 122ms
typeclass inference of ZeroHomClass took 425ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 109ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 137ms
elaboration took 102ms
typeclass inference of Group took 413ms
typeclass inference of Group took 194ms
typeclass inference of AddCommGroup took 306ms
tactic execution of Lean.Parser.Tactic.exact took 168ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 536ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 138ms
type checking took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 181ms
tactic execution of Lean.Parser.Tactic.change took 109ms
typeclass inference of Group took 247ms
typeclass inference of AddCommGroup took 398ms
typeclass inference of Group took 505ms
typeclass inference of Group took 199ms
typeclass inference of AddCommMonoid took 114ms
typeclass inference of AddCommMonoid took 110ms
tactic execution of Lean.Parser.Tactic.change took 398ms
tactic execution of Lean.Parser.Tactic.exact took 317ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 189ms
typeclass inference of Group took 200ms
typeclass inference of Group took 258ms
typeclass inference of AddCommGroup took 335ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.8s
tactic execution of Lean.Parser.Tactic.exact took 105ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 283ms
typeclass inference of AddHomClass took 123ms
typeclass inference of StarHomClass took 183ms
typeclass inference of MulActionHomClass took 125ms
type checking took 116ms
type checking took 108ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 108ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 258ms
typeclass inference of NonUnitalNonAssocSemiring took 381ms
typeclass inference of Semiring took 223ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 197ms
typeclass inference of ZeroHomClass took 165ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 134ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 126ms
typeclass inference of Group took 606ms
typeclass inference of Group took 195ms
typeclass inference of Group took 403ms
typeclass inference of Group took 200ms
typeclass inference of Group took 283ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 285ms
typeclass inference of Group took 657ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 150ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 154ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 121ms
tactic execution of Lean.Parser.Tactic.exact took 154ms
typeclass inference of Group took 197ms
typeclass inference of Monoid took 405ms
typeclass inference of AddCommGroup took 490ms
typeclass inference of AddCommGroup took 540ms
typeclass inference of AddCommGroup took 491ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 140ms
typeclass inference of AddCommGroup took 406ms
typeclass inference of Group took 246ms
typeclass inference of Group took 212ms
typeclass inference of AddGroup took 197ms
typeclass inference of Monoid took 407ms
typeclass inference of Monoid took 400ms
typeclass inference of Monoid took 487ms
typeclass inference of AddCommGroup took 430ms
typeclass inference of AddMonoid took 278ms
typeclass inference of AddMonoid took 288ms
typeclass inference of AddZeroClass took 429ms
typeclass inference of AddMonoid took 423ms
typeclass inference of AddZeroClass took 428ms
typeclass inference of AddMonoid took 424ms
typeclass inference of Group took 404ms
typeclass inference of Group took 188ms
typeclass inference of Monoid took 413ms
typeclass inference of Monoid took 250ms
cumulative profiling times:
	aesop 52.5ms
	attribute application 39.8ms
	blocked (unaccounted) 4.35s
	compilation (IR) 3.38ms
	compilation (LCNF base) 68.9ms
	compilation (LCNF impure) 13.3ms
	compilation (LCNF mono) 32.8ms
	congr simp thm 92.4ms
	dsimp 12.3ms
	elaboration 3.42s
	fix level params 50.9ms
	import 1.41s
	initialization 32.5ms
	instantiate metavars 49.9ms
	interpretation 4.5s
	let-to-have transformation 68.5ms
	linting 462ms
	module linting 0.00127ms
	norm_num 130ms
	overlappingInstancesLinter 127ms
	parsing 368ms
	process pre-definitions 734ms
	ring 71.3ms
	share common exprs 216ms
	simp 2.42s
	tactic execution 13.6s
	tacticAnalysis 781ms
	type checking 6.22s
	typeclass inference 52.8s
real 41.73
user 87.15
sys 1.34

`LeanPool/InfiniteConnesRigidity/GroupConstruction.lean`

import took 1.45s
type checking took 215ms
simp took 110ms
tactic execution of Lean.Parser.Tactic.change took 151ms
tactic execution of Lean.Parser.Tactic.change took 144ms
tactic execution of Lean.Parser.Tactic.change took 197ms
tactic execution of Lean.Parser.Tactic.change took 124ms
typeclass inference of MeasurableSingletonClass took 103ms
tactic execution of Lean.Parser.Tactic.refine took 166ms
typeclass inference of MulOne took 128ms
typeclass inference of MulOne took 107ms
simp took 859ms
tactic execution of Lean.Parser.Tactic.refine took 122ms
simp took 2.27s
simp took 1.89s
typeclass inference of StarHomClass took 263ms
typeclass inference of StarHomClass took 255ms
tactic execution of Lean.Parser.Tactic.obtain took 695ms
tactic execution of Lean.Parser.Tactic.exact took 131ms
type checking took 115ms
tactic execution of Lean.Parser.Tactic.change took 143ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 690ms
typeclass inference of Monoid took 399ms
typeclass inference of Monoid took 666ms
typeclass inference of Monoid took 400ms
typeclass inference of ZeroHomClass took 402ms
typeclass inference of ZeroHomClass took 404ms
typeclass inference of ZeroHomClass took 409ms
typeclass inference of Monoid took 403ms
typeclass inference of AddZeroClass took 697ms
typeclass inference of Monoid took 389ms
typeclass inference of AddGroup took 329ms
typeclass inference of AddCommGroup took 459ms
typeclass inference of Monoid took 437ms
simp took 615ms
simp took 616ms
simp took 593ms
simp took 588ms
simp took 544ms
simp took 697ms
simp took 698ms
simp took 683ms
simp took 744ms
simp took 758ms
simp took 607ms
simp took 520ms
simp took 417ms
simp took 549ms
simp took 542ms
simp took 388ms
type checking took 133ms
typeclass inference of AddCommMonoid took 128ms
typeclass inference of AddCommMonoid took 135ms
typeclass inference of Group took 302ms
typeclass inference of Group took 187ms
typeclass inference of ZeroHomClass took 113ms
typeclass inference of ZeroHomClass took 103ms
typeclass inference of ZeroHomClass took 279ms
typeclass inference of ZeroHomClass took 279ms
typeclass inference of ZeroHomClass took 217ms
typeclass inference of ZeroHomClass took 274ms
typeclass inference of AddHomClass took 115ms
typeclass inference of ZeroHomClass took 109ms
typeclass inference of AddZero took 422ms
typeclass inference of AddZeroClass took 700ms
typeclass inference of AddZeroClass took 414ms
typeclass inference of AddZeroClass took 504ms
typeclass inference of AddZeroClass took 272ms
typeclass inference of AddZero took 424ms
typeclass inference of AddZeroClass took 578ms
typeclass inference of AddZeroClass took 253ms
typeclass inference of AddZero took 288ms
typeclass inference of AddCommGroup took 507ms
typeclass inference of CommRing took 138ms
typeclass inference of Semiring took 194ms
typeclass inference of Module.Projective took 425ms
typeclass inference of AddZero took 257ms
typeclass inference of AddZeroClass took 433ms
typeclass inference of AddZeroClass took 253ms
cumulative profiling times:
	aesop 600ms
	attribute application 54.8ms
	blocked (unaccounted) 3.38s
	compilation (IR) 5.72ms
	compilation (LCNF base) 111ms
	compilation (LCNF impure) 26ms
	compilation (LCNF mono) 69.5ms
	congr simp thm 124ms
	dsimp 98.8ms
	elaboration 3.76s
	fix level params 71ms
	import 1.45s
	initialization 31.8ms
	instantiate metavars 98.7ms
	interpretation 8.1s
	let-to-have transformation 15.8ms
	linting 893ms
	module linting 0.0011ms
	norm_num 759ms
	overlappingInstancesLinter 169ms
	parsing 599ms
	process pre-definitions 747ms
	ring 414ms
	share common exprs 374ms
	simp 17.2s
	tactic execution 13.9s
	tacticAnalysis 1.38s
	type checking 4.21s
	typeclass inference 58.4s
real 33.66
user 111.85
sys 1.68

`LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean`

import took 1.37s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 164ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 529ms
type checking took 111ms
typeclass inference of NonUnitalNonAssocSemiring took 195ms
typeclass inference of Semiring took 148ms
elaboration took 128ms
typeclass inference of NonUnitalNonAssocSemiring took 163ms
typeclass inference of Semiring took 146ms
typeclass inference of NonUnitalNonAssocSemiring took 161ms
typeclass inference of Semiring took 147ms
typeclass inference of NonUnitalNonAssocSemiring took 163ms
typeclass inference of Semiring took 146ms
simp took 189ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 161ms
tactic execution of Mathlib.Tactic.nlinarith took 170ms
typeclass inference of NonUnitalNonAssocSemiring took 289ms
typeclass inference of Semiring took 263ms
typeclass inference of NonUnitalNonAssocSemiring took 281ms
typeclass inference of Semiring took 251ms
typeclass inference of NonUnitalNonAssocSemiring took 298ms
typeclass inference of Semiring took 261ms
typeclass inference of NonUnitalNonAssocSemiring took 182ms
typeclass inference of Semiring took 154ms
tactic execution of Lean.Parser.Tactic.exact took 139ms
typeclass inference of NonUnitalNonAssocSemiring took 270ms
typeclass inference of Semiring took 150ms
tactic execution of Lean.Parser.Tactic.exact took 203ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 578ms
typeclass inference of CommMonoid took 302ms
typeclass inference of NonUnitalNonAssocSemiring took 211ms
typeclass inference of Semiring took 158ms
typeclass inference of StarHomClass took 165ms
elaboration took 142ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 147ms
type checking took 241ms
tactic execution of Lean.Parser.Tactic.refine took 129ms
tactic execution of Lean.Parser.Tactic.change took 121ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 112ms
type checking took 190ms
typeclass inference of NonUnitalNonAssocSemiring took 260ms
typeclass inference of Semiring took 175ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 367ms
typeclass inference of NonUnitalNonAssocSemiring took 162ms
typeclass inference of Semiring took 142ms
tactic execution of Lean.Parser.Tactic.refine took 164ms
tactic execution of Lean.Parser.Tactic.exact took 113ms
typeclass inference of NonUnitalNonAssocSemiring took 170ms
typeclass inference of Semiring took 153ms
typeclass inference of NonUnitalNonAssocSemiring took 205ms
typeclass inference of Semiring took 151ms
typeclass inference of NonUnitalNonAssocSemiring took 253ms
typeclass inference of Semiring took 150ms
typeclass inference of NonUnitalNonAssocSemiring took 258ms
typeclass inference of Semiring took 147ms
typeclass inference of NonUnitalNonAssocSemiring took 177ms
typeclass inference of Semiring took 145ms
elaboration took 100ms
typeclass inference of NonUnitalNonAssocSemiring took 167ms
typeclass inference of Semiring took 148ms
typeclass inference of NonUnitalNonAssocSemiring took 168ms
typeclass inference of Semiring took 150ms
typeclass inference of NonUnitalNonAssocSemiring took 165ms
typeclass inference of Semiring took 145ms
typeclass inference of NonUnitalNonAssocSemiring took 168ms
typeclass inference of Semiring took 148ms
simp took 414ms
simp took 407ms
simp took 274ms
simp took 136ms
simp took 198ms
simp took 110ms
simp took 602ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 364ms
typeclass inference of NonUnitalNonAssocSemiring took 282ms
typeclass inference of Semiring took 256ms
simp took 103ms
simp took 115ms
simp took 105ms
simp took 140ms
simp took 107ms
simp took 103ms
type checking took 152ms
typeclass inference of NonUnitalNonAssocSemiring took 103ms
typeclass inference of MulHomClass took 113ms
simp took 130ms
simp took 131ms
cumulative profiling times:
	aesop 60.6ms
	attribute application 58.4ms
	blocked (unaccounted) 3.69s
	compilation (IR) 2.02ms
	compilation (LCNF base) 37ms
	compilation (LCNF impure) 9ms
	compilation (LCNF mono) 27.6ms
	congr simp thm 240ms
	dsimp 101ms
	elaboration 5.83s
	fix level params 111ms
	import 1.37s
	initialization 35.9ms
	instantiate metavars 186ms
	interpretation 8.79s
	let-to-have transformation 31.9ms
	linting 888ms
	module linting 0.00128ms
	norm_num 260ms
	overlappingInstancesLinter 245ms
	parsing 585ms
	process pre-definitions 894ms
	ring 375ms
	share common exprs 414ms
	simp 10s
	tactic execution 14.5s
	tacticAnalysis 1.45s
	type checking 8.13s
	typeclass inference 58.4s
real 47.41
user 112.69
sys 1.54

`LeanPool/InfiniteConnesRigidity/UniversalLattice.lean`

import took 1.26s
tactic execution of Lean.Parser.Tactic.exact took 7.12s
tactic execution of Lean.Parser.Tactic.exact took 6.93s
congr simp thm took 192ms
elaboration took 822ms
typeclass inference of NonUnitalNonAssocSemiring took 168ms
typeclass inference of Semiring took 147ms
simp took 105ms
simp took 123ms
simp took 119ms
simp took 102ms
simp took 169ms
simp took 106ms
typeclass inference of HSMul took 120ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 165ms
tactic execution of Lean.Parser.Tactic.refine took 114ms
tactic execution of Lean.Parser.Tactic.refine took 128ms
tactic execution of Lean.Parser.Tactic.refine took 146ms
tactic execution of Lean.Parser.Tactic.refine took 185ms
tactic execution of Lean.Parser.Tactic.refine took 203ms
tactic execution of Lean.Parser.Tactic.refine took 237ms
tactic execution of Lean.Parser.Tactic.refine took 237ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 109ms
tactic execution of Lean.Parser.Tactic.refine took 175ms
instantiate metavars took 154ms
share common exprs took 104ms
process pre-definitions took 119ms
elaboration took 133ms
type checking took 599ms
simp took 840ms
simp took 968ms
simp took 738ms
simp took 733ms
simp took 873ms
simp took 617ms
simp took 589ms
simp took 721ms
simp took 493ms
type checking took 127ms
simp took 655ms
simp took 636ms
simp took 612ms
simp took 684ms
simp took 699ms
simp took 679ms
simp took 522ms
simp took 528ms
simp took 526ms
simp took 144ms
simp took 219ms
simp took 142ms
simp took 140ms
simp took 218ms
simp took 134ms
simp took 133ms
simp took 199ms
simp took 129ms
simp took 345ms
simp took 402ms
simp took 255ms
simp took 259ms
simp took 261ms
simp took 259ms
simp took 148ms
simp took 110ms
simp took 110ms
simp took 110ms
simp took 135ms
type checking took 129ms
elaboration took 132ms
simp took 108ms
simp took 114ms
simp took 108ms
simp took 125ms
simp took 105ms
simp took 104ms
simp took 120ms
simp took 119ms
simp took 121ms
simp took 113ms
simp took 111ms
simp took 102ms
simp took 109ms
simp took 569ms
simp took 506ms
simp took 535ms
simp took 433ms
simp took 466ms
simp took 468ms
simp took 466ms
simp took 466ms
simp took 508ms
simp took 513ms
simp took 510ms
simp took 510ms
simp took 372ms
simp took 372ms
simp took 370ms
simp took 368ms
type checking took 141ms
cumulative profiling times:
	attribute application 70.6ms
	blocked (unaccounted) 11.1s
	compilation (IR) 4.39ms
	compilation (LCNF base) 108ms
	compilation (LCNF impure) 20.6ms
	compilation (LCNF mono) 67.7ms
	congr simp thm 430ms
	dsimp 355ms
	elaboration 5.55s
	fix level params 218ms
	import 1.26s
	initialization 29.7ms
	instantiate metavars 492ms
	interpretation 11.5s
	let-to-have transformation 59.2ms
	linting 1.05s
	module linting 0.00155ms
	norm_num 47.8ms
	overlappingInstancesLinter 259ms
	parsing 631ms
	process pre-definitions 1.03s
	ring 567ms
	share common exprs 691ms
	simp 38.1s
	tactic execution 27.8s
	tacticAnalysis 1.48s
	type checking 6s
	typeclass inference 41.8s
real 59.04
user 137.96
sys 1.68

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

github-actions · 2026-09-04T12:52:25Z

🤖 LLM review (`gpt-5.6-sol`, 5 rubrics)

Reviewed head: 6f79b15eb330c5f04eb15976c87070c28bc0d1a4

⚠️ Partial review — diff exceeded the size budget. The bodies of the 1 largest of 8 file patches were elided before review; an elided review cannot approve.

Verdict: 🤔 needs_discussion — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	🤔 `discuss`	Based on the partial diff, the visible theorem signatures match the card, but faithfulness remains unverifiable until the elided foundational module is reviewed.
Novelty	✅ `pass`	Based on the partial diff, the completed Mathlib searches contain no theorem matching either headline, and the only pool overlap is the weaker listed conditional Connes-rigidity project.
Significance	✅ `pass`	This is a research-level, named Connes-rigidity result with a completed infinite-family endpoint; the assessment is based on the visible content of a partial diff.
Sources	✅ `pass`	Based on the partial diff, the exact OpenAI commit and Dean Cureton baseline are credited consistently, but the cited repository’s theorem statement is not independently verifiable from the visible content.
Code quality (advisory)	🤔 `discuss`	Based on the partial diff, exact duplicate helpers across the visible modules, dead endpoint wrappers, and an unused model field leave enough maintenance debt for human review.

Aspect	Value
Proves the claim	➖ `unverifiable`
Matches cited source	🟡 `unverifiable`
Fit	✅ `good_fit`
Level	`research`
Branch	operator algebras and geometric group theory
Mode	`theory_building`
Code quality	2 / 5

Statement check: The visible headline unconditionally produces Λ and an ℕ-indexed Γ with finite generation, ICC, property (T), factor isomorphisms, pairwise nonisomorphism, and nonisomorphism to Λ exactly as claimed.

The contribution constructs a distinguished property-(T) ICC group and an infinite pairwise nonisomorphic family with mutually isomorphic tracial group von Neumann algebras, supported by a substantial development of property (T), group constructions, Fourier analysis, and factor equivalences.

Faithfulness findings (1)

partial-diff-unverifiable — LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean:5225
The headline has no explicit hypotheses and its visible quantifiers and conjuncts match the card, but the declarations defining its central semantic predicates are not present in the visible diff; 9,032 lines of the foundational UniversalLattice.lean patch are elided. This prevents checking whether the predicates encode the claimed mathematical objects rather than surrogates or postulated content. Re-review the full foundational module; the visible headline itself requires no card correction.
Evidence: The visible declaration begins theorem exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors : and quantifies ∃ (Λ : ConnesRigidity.CountableDiscreteGroup.{0}) with (Γ : ℕ → ConnesRigidity.CountableDiscreteGroup.{0}),, including (∀ n, ConnesRigidity.TracialGroupFactorsIsomorphic (Γ n) Λ) ∧; the foundational patch is replaced by [elided by lean-pool llm-review: 9,032 of 9,072 patch lines omitted — diff exceeded the review size budget].

Code quality findings (3)

duplicate-definition — PR-wide
The visible modules repeatedly define the same abstraction or lemma under different names. Consolidate these into shared helpers instead of maintaining parallel proofs. In particular, FactorAndRigidity imports GroupConstruction, and GroupConstruction imports CarryAndCrossedProduct, so dualPointAction, kEAddAction, and the private normality proof can reuse the existing declarations. The same-file duplicates for character integrals, clipping, and idempotence should be removed directly.
Evidence: Exact duplicates include:

public
def carryEAddAction (n : ℕ) (k : K) : E n ≃+ E n :=
MulEquiv.toAdditive (kEAction n k)

private def kEAddAction (n : ℕ) (k : K) : E n ≃+ E n :=
MulEquiv.toAdditive (kEAction n k)

private def dualPointAction (k : K) (z : X × Y) : X × Y :=
(z.1.comp (kLinear k⁻¹).toLinearMap,
z.2.comp (kDividedSquareLinear k⁻¹).toLinearMap)

public
noncomputable def dualPairAction (k : K) (z : X × Y) : X × Y :=
(z.1.comp (kLinear k⁻¹).toLinearMap,
z.2.comp (kDividedSquareLinear k⁻¹).toLinearMap)

Both PaperFactorUnitaryWitness.starAlgEquiv_isNormal and the imported public theorem have the signature:

(e : A ≃⋆ₐ[ℂ] B) :
IsNormalStarAlgEquiv e

The same file also contains both integral_add_character_eq_zero and split_integral_character_eq_zero with the same generic statement and proof, as well as:

private def complexUnitBallClip (z : ℂ) : ℂ :=
(1 / max 1 ‖z‖ : ℝ) • z

private def clip (z : ℂ) : ℂ :=
(1 / max 1 ‖z‖ : ℝ) • z

and the duplicate statements:

private theorem scalar_mul_self (c : F) : c * c = c := by

private theorem binary_sq_eq_self (a : F) : a * a = a := by

The exponent-injectivity argument is likewise duplicated as paperInvariantCard_injective and two_pow_four_injective, both proving (h : 2 ^ (4 * m) = 2 ^ (4 * n)) : m = n.

unused-declaration — LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean:5140
The PaperAnalyticInput namespace contains five private wrapper theorems that have no downstream consumer. The actual assembly path only calls input.universalLattice, then paperFamilyInput_of_universalLattice. Remove lambda_propertyT, gamma_propertyT, lambda_icc, gamma_icc, and gamma_not_isomorphic_lambda, or make the assembly use them instead of recomputing the same facts through PaperFamilyInput.
Evidence: The dead wrappers are declared as:

private theorem lambda_propertyT (input : PaperAnalyticInput) :
HasKazhdanPropertyT lambdaGroup :=
lambda_hasKazhdanPropertyT_unconditional input.universalLattice

private theorem gamma_propertyT (input : PaperAnalyticInput) (n : ℕ) :
HasKazhdanPropertyT (gammaGroup n) :=
gamma_hasKazhdanPropertyT_unconditional n input.universalLattice

private theorem lambda_icc : IsICC lambdaGroup :=
lambda_isICC

private theorem gamma_icc (n : ℕ) : IsICC (gammaGroup n) :=
gamma_isICC n

private theorem gamma_not_isomorphic_lambda (n : ℕ) :
¬GroupsIsomorphic (gammaGroup n) lambdaGroup :=
not_groupsIsomorphic_of_orderFour (gamma_has_order_four n)
paperLambda_orderOf_ne_four

The only downstream construction is:

private def toPaperFamilyInput (input : PaperAnalyticInput) :
PaperFamilyInput :=
paperFamilyInput_of_universalLattice input.universalLattice

private def infinitePropertyTFiber (input : PaperAnalyticInput) :
InfinitePropertyTFiber :=
input.toPaperFamilyInput.toInfinitePropertyTFiber

unused-structure-field — PR-wide
CrossedProductModel.trace is constructed but never consumed; the later transport layer discards it and builds a separate pointed model from only .algebra and crossedVacuum. This leaves two overlapping model abstractions and an unmaintained trace field. Consolidate the crossed-product model around the algebra and vacuum, or use the stored trace in the transport and trace-preservation proofs.
Evidence: The field is introduced by:

public
structure CrossedProductModel
(ℋ : Type v)
[NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] where
/-- The modeled von Neumann algebra. -/
algebra : VonNeumannAlgebra ℋ
/-- The trace on the modeled algebra. -/
trace : algebra.toStarSubalgebra → ℂ

It is populated by:

public
def crossedProductModel (X : HaarProbabilityAction K Ω) :
CrossedProductModel (crossedHilbert X) where
algebra := vonNeumannClosure (crossedGeneratorSet X)
trace := fun T ↦ inner ℂ (crossedVacuum X)
((T : crossedHilbert X →L[ℂ] crossedHilbert X) (crossedVacuum X))

but the downstream representation immediately discards it:

private def crossedPointedModel
{J : Type u} [Group J]
{Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω]
(A : HaarProbabilityAction J Ω) :
PointedVonNeumannModel (crossedHilbert A) where
algebra := (crossedProductModel A).algebra
vacuum := crossedVacuum A

Tokens: 2,179,624 in / 23,516 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $11.4272
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

Vilin97 · 2026-09-04T14:31:53Z

/review

github-actions · 2026-09-04T14:32:08Z

LLM review skipped: Lean Action CI conclusion was in_progress. Push a fix or comment /review after CI is green.

Vilin97 · 2026-09-04T14:34:07Z

Automation disposition: needs-maintainer

Reviewed exact head 0d9e99d after a verified repair pass that removed inert sections and unused assumptions; all four affected modules build. Duplicate character/clip/injectivity/normality paths and the unconsumed public spectral-measure framework remain, while UniversalLattice is still elided from the size-limited review. That is architectural work below the 4/5 target.

feat: import infinite Connes rigidity proof

3181ff2

Remove inert rigidity scaffolding

0d9e99d

Vilin97 added the needs-maintainer Requires a maintainer decision; automation must not merge label Sep 4, 2026

github-actions Bot added 5 commits September 4, 2026 14:35

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

ec333fb

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

030c88f

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

d9bcd76

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

6f79b15

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

92170e7

Navigation Menu

Import OpenAI infinite Connes rigidity formalization - #393

Import OpenAI infinite Connes rigidity formalization#393
Vilin97 wants to merge 7 commits into
mainfrom
codex/import-openai-connes-infinite-rigidity-2026-09-04

Vilin97 commented Sep 4, 2026

Uh oh!

greptile-apps Bot commented Sep 4, 2026 •

edited

Loading

Important Files Changed

Uh oh!

github-actions Bot commented Sep 4, 2026

`LeanPool/InfiniteConnesRigidity.lean`

`LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean`

`LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean`

`LeanPool/InfiniteConnesRigidity/GroupConstruction.lean`

`LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean`

`LeanPool/InfiniteConnesRigidity/UniversalLattice.lean`

Uh oh!

github-actions Bot commented Sep 4, 2026 •

edited

Loading

Uh oh!

Vilin97 commented Sep 4, 2026

Uh oh!

github-actions Bot commented Sep 4, 2026

Uh oh!

Vilin97 commented Sep 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

Vilin97 commented Sep 4, 2026

Summary

Provenance

Existing pooled project and reuse experiment

Reduction and optimization

Verification

Uh oh!

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

Uh oh!

Greptile Summary

Important Files Changed

Uh oh!

github-actions Bot commented Sep 4, 2026

Proof profile (new / modified Lean files)

Aggregate phase totals

Slowest changed modules (from lake build)

LeanPool/InfiniteConnesRigidity.lean

LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean

LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean

LeanPool/InfiniteConnesRigidity/GroupConstruction.lean

LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean

LeanPool/InfiniteConnesRigidity/UniversalLattice.lean

Uh oh!

github-actions Bot commented Sep 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 LLM review (gpt-5.6-sol, 5 rubrics)

Faithfulness findings (1)

Code quality findings (3)

Uh oh!

Vilin97 commented Sep 4, 2026

Uh oh!

github-actions Bot commented Sep 4, 2026

Uh oh!

Vilin97 commented Sep 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

greptile-apps Bot commented Sep 4, 2026 •

edited

Loading

Slowest changed modules (from `lake build`)

`LeanPool/InfiniteConnesRigidity.lean`

`LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean`

`LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean`

`LeanPool/InfiniteConnesRigidity/GroupConstruction.lean`

`LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean`

`LeanPool/InfiniteConnesRigidity/UniversalLattice.lean`

github-actions Bot commented Sep 4, 2026 •

edited

Loading

🤖 LLM review (`gpt-5.6-sol`, 5 rubrics)