Repository navigation
Import polylean formalization - #109
Conversation
Proof profile (new / modified Lean files)
This is the parallel build wall clock and is the compile-time answer for this PR. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 3,936 maxHeartbeats units across 13 files (3,416 added LOC). Sum of Count-heartbeats wall-clock total: 211.46 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Polylean.UnitConjecture.GardamTheorem |
181.00 s |
LeanPool.Polylean.UnitConjecture |
9.50 s |
LeanPool.Polylean.UnitConjecture.FreeModule |
5.10 s |
LeanPool.Polylean.UnitConjecture.Cocycle |
4.40 s |
LeanPool.Polylean.UnitConjecture.GardamGroup |
3.60 s |
LeanPool.Polylean.UnitConjecture.MetabelianGroup |
3.40 s |
LeanPool.Polylean.UnitConjecture.TorsionFree |
3.00 s |
LeanPool.Polylean.UnitConjecture.GroupRing |
2.70 s |
LeanPool.Polylean.UnitConjecture.AddFreeGroup |
2.50 s |
LeanPool.Polylean |
2.50 s |
LeanPool.Polylean.UnitConjecture.Tactics |
2.00 s |
LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets |
1.50 s |
Per-file `lean --profile` output
LeanPool/Polylean.lean
import took 2.25s
cumulative profiling times:
elaboration 0.141ms
import 2.25s
initialization 28.5ms
interpretation 214ms
linting 0.269ms
parsing 0.0352ms
real 3.56
user 1.91
sys 1.44
LeanPool/Polylean/UnitConjecture.lean
import took 2.25s
cumulative profiling times:
elaboration 0.153ms
import 2.25s
initialization 28.7ms
interpretation 214ms
linting 0.215ms
parsing 0.0474ms
real 3.21
user 1.87
sys 1.36
LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean
import took 1.12s
cumulative profiling times:
attribute application 0.675ms
blocked (unaccounted) 0.966ms
compilation (IR) 0.531ms
compilation (LCNF base) 5.09ms
compilation (LCNF impure) 2.08ms
compilation (LCNF mono) 5.05ms
congr simp thm 0.74ms
dsimp 11.4ms
elaboration 67.1ms
fix level params 0.546ms
import 1.12s
initialization 28.3ms
instantiate metavars 1.51ms
interpretation 155ms
let-to-have transformation 1.56ms
linting 4.7ms
parsing 6.28ms
process pre-definitions 8.96ms
share common exprs 1.19ms
simp 17.5ms
tactic execution 82.7ms
type checking 28ms
typeclass inference 122ms
real 2.21
user 1.47
sys 0.82
LeanPool/Polylean/UnitConjecture/Cocycle.lean
import took 2.25s
cumulative profiling times:
aesop 29.6ms
attribute application 0.658ms
blocked (unaccounted) 283ms
congr simp thm 1.03ms
elaboration 58.9ms
fix level params 0.546ms
import 2.25s
initialization 28.6ms
instantiate metavars 0.382ms
interpretation 388ms
let-to-have transformation 0.126ms
linting 6.42ms
parsing 11ms
process pre-definitions 2.44ms
share common exprs 1.2ms
simp 47ms
tactic execution 25.4ms
type checking 24.7ms
typeclass inference 342ms
real 3.75
user 2.53
sys 1.38
LeanPool/Polylean/UnitConjecture/EnumDecide.lean
import took 201ms
cumulative profiling times:
attribute application 1.93ms
blocked (unaccounted) 0.211ms
compilation (IR) 0.575ms
compilation (LCNF base) 4.3ms
compilation (LCNF impure) 2.56ms
compilation (LCNF mono) 4.74ms
congr simp thm 0.102ms
elaboration 44ms
fix level params 0.28ms
import 201ms
initialization 28.3ms
instantiate metavars 0.847ms
interpretation 2.94ms
let-to-have transformation 1.28ms
linting 6.03ms
parsing 7.25ms
process pre-definitions 21.1ms
share common exprs 1.02ms
simp 0.373ms
tactic execution 48.5ms
type checking 29.2ms
typeclass inference 30.8ms
real 0.94
user 0.58
sys 0.45
LeanPool/Polylean/UnitConjecture/FreeModule.lean
import took 1.02s
cumulative profiling times:
attribute application 5.87ms
blocked (unaccounted) 570ms
compilation (IR) 3.37ms
compilation (LCNF base) 54.5ms
compilation (LCNF impure) 17.6ms
compilation (LCNF mono) 38.8ms
congr simp thm 21ms
elaboration 530ms
fix level params 4.14ms
import 1.02s
initialization 28.6ms
instantiate metavars 8.75ms
interpretation 958ms
let-to-have transformation 61.9ms
linting 85.3ms
parsing 67.7ms
process pre-definitions 200ms
share common exprs 17.9ms
simp 288ms
tactic execution 1.1s
type checking 153ms
typeclass inference 875ms
real 3.27
user 5.35
sys 0.93
LeanPool/Polylean/UnitConjecture/GardamGroup.lean
import took 2.26s
tactic execution of Lean.Parser.Tactic.decide took 144ms
type checking took 103ms
cumulative profiling times:
attribute application 23ms
blocked (unaccounted) 34.8ms
compilation (IR) 1.73ms
compilation (LCNF base) 48.4ms
compilation (LCNF impure) 9.61ms
compilation (LCNF mono) 19.8ms
congr simp thm 1.37ms
elaboration 195ms
fix level params 0.354ms
import 2.26s
initialization 30.2ms
instantiate metavars 0.555ms
interpretation 500ms
let-to-have transformation 0.446ms
linting 8.77ms
norm_num 1.5ms
parsing 15.3ms
process pre-definitions 9.63ms
share common exprs 2.35ms
simp 29.2ms
tactic execution 203ms
type checking 166ms
typeclass inference 498ms
real 4.34
user 3.35
sys 1.43
LeanPool/Polylean/UnitConjecture/GardamTheorem.lean
import took 2.25s
type checking took 93.6s
type checking took 87.5s
cumulative profiling times:
aesop 32.3ms
attribute application 0.95ms
blocked (unaccounted) 94s
compilation (IR) 2.29ms
compilation (LCNF base) 65.2ms
compilation (LCNF impure) 8.61ms
compilation (LCNF mono) 27.5ms
congr simp thm 2.52ms
elaboration 120ms
fix level params 0.494ms
import 2.25s
initialization 28.4ms
instantiate metavars 1.32ms
interpretation 609ms
let-to-have transformation 0.595ms
linting 38ms
parsing 15ms
process pre-definitions 26.2ms
share common exprs 2.86ms
simp 73.7ms
tactic execution 205ms
type checking 181s
typeclass inference 315ms
real 185.18
user 160.27
sys 13.68
LeanPool/Polylean/UnitConjecture/GroupRing.lean
import took 1.19s
cumulative profiling times:
attribute application 2.39ms
blocked (unaccounted) 22.1ms
compilation (IR) 1.04ms
compilation (LCNF base) 14.1ms
compilation (LCNF impure) 4.78ms
compilation (LCNF mono) 15.1ms
congr simp thm 7.11ms
dsimp 1.33ms
elaboration 172ms
fix level params 1.55ms
import 1.19s
initialization 28.4ms
instantiate metavars 6.52ms
interpretation 413ms
let-to-have transformation 1.84ms
linting 29.5ms
parsing 24.1ms
process pre-definitions 75.4ms
share common exprs 10.7ms
simp 306ms
tactic execution 527ms
type checking 125ms
typeclass inference 414ms
real 3.05
user 3.05
sys 0.92
LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean
import took 2.44s
cumulative profiling times:
aesop 38.3ms
attribute application 0.278ms
blocked (unaccounted) 373ms
compilation (IR) 0.295ms
compilation (LCNF base) 4.98ms
compilation (LCNF impure) 1.24ms
compilation (LCNF mono) 3.65ms
congr simp thm 1.28ms
elaboration 48.6ms
fix level params 0.861ms
import 2.44s
initialization 28.8ms
instantiate metavars 0.68ms
interpretation 311ms
let-to-have transformation 0.0895ms
linting 3.9ms
parsing 7.18ms
process pre-definitions 5.55ms
share common exprs 1.61ms
simp 112ms
tactic execution 19.7ms
type checking 23.4ms
typeclass inference 259ms
real 3.92
user 2.43
sys 1.44
LeanPool/Polylean/UnitConjecture/Tactics.lean
import took 927ms
cumulative profiling times:
elaboration 0.154ms
import 927ms
initialization 28.3ms
interpretation 19.6ms
linting 0.145ms
parsing 0.0323ms
real 1.58
user 0.83
sys 0.76
LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean
import took 922ms
cumulative profiling times:
attribute application 0.0941ms
compilation (IR) 0.277ms
compilation (LCNF base) 11.1ms
compilation (LCNF impure) 1.63ms
compilation (LCNF mono) 2.99ms
elaboration 0.496ms
fix level params 0.0225ms
import 922ms
initialization 28.3ms
instantiate metavars 0.0237ms
interpretation 31.7ms
let-to-have transformation 0.0392ms
linting 0.489ms
parsing 0.158ms
process pre-definitions 0.845ms
share common exprs 0.0915ms
type checking 0.489ms
typeclass inference 2.54ms
real 1.59
user 0.86
sys 0.76
LeanPool/Polylean/UnitConjecture/TorsionFree.lean
import took 2.22s
cumulative profiling times:
attribute application 0.909ms
blocked (unaccounted) 136ms
compilation (IR) 0.164ms
compilation (LCNF base) 3.19ms
compilation (LCNF impure) 0.87ms
compilation (LCNF mono) 1.89ms
congr simp thm 0.97ms
elaboration 165ms
fix level params 0.403ms
import 2.22s
initialization 28.1ms
instantiate metavars 0.976ms
interpretation 360ms
let-to-have transformation 0.105ms
linting 7.94ms
parsing 11.9ms
process pre-definitions 4.73ms
share common exprs 1.99ms
simp 73ms
tactic execution 120ms
type checking 51.4ms
typeclass inference 212ms
real 3.63
user 2.57
sys 1.43
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
There was a problem hiding this comment.
Pull request overview
This PR vendors the Polylean formalization infrastructure around Gardam’s disproof of Kaplansky’s Unit Conjecture, adding the Promislow/Hantzsche–Wendt group construction, free-module and group-ring development, and the torsion-freeness result into LeanPool under a new polylean project entry.
Changes:
- Add a new
polyleanproject card and entry module (LeanPool.Polylean) referencing the upstream repository. - Introduce the Unit Conjecture infrastructure: metabelian group construction of
P, free modules and group rings, plus tactics support. - Prove torsion-freeness of the Promislow group (
LeanPool.Polylean.P.torsionFree) and wire the new modules into the root imports.
Assessment (Lean Pool REVIEW_RULES.md):
- Fit: good_fit
- Level: research
- Branch: algebra (group theory / ring theory)
- Mode: theory_building
- Obscure problem: false
- Code quality: 2/5
- Significance: Vendors a paper-anchored formal development supporting Gardam’s unit-conjecture counterexample, with the main theorem being torsion-freeness of the Promislow group.
- Verdict: request_changes
Reviewed changes
Copilot reviewed 14 out of 14 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| LeanPool/projects.yml | Adds the polylean project entry and metadata. |
| LeanPool/Polylean.lean | Entry-point module and project card for the imported library. |
| LeanPool/Polylean/UnitConjecture.lean | Import-only index + narrative doc for the Polylean Unit Conjecture infrastructure. |
| LeanPool/Polylean/UnitConjecture/TorsionFree.lean | Defines torsion-free notions and proves P is torsion-free. |
| LeanPool/Polylean/UnitConjecture/GardamGroup.lean | Constructs the Promislow group P as a metabelian extension. |
| LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean | General metabelian group construction from an action and cocycle. |
| LeanPool/Polylean/UnitConjecture/Cocycle.lean | Defines actions by automorphisms and cocycles + basic lemmas. |
| LeanPool/Polylean/UnitConjecture/EnumDecide.lean | Adds an enumeration-based mechanism to decide ∀ x, P x for finite/compact types. |
| LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean | Defines free abelian groups and decidable equality of homs on finitely generated free groups. |
| LeanPool/Polylean/UnitConjecture/FreeModule.lean | Implements free modules as quotients of formal sums, with decidable equality and coordinates. |
| LeanPool/Polylean/UnitConjecture/GroupRing.lean | Constructs group rings R[G] from the free-module quotient and proves ring structure. |
| LeanPool/Polylean/UnitConjecture/Tactics.lean | Import-only index for local tactics. |
| LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean | Declares local Aesop rule sets used by the development. |
| LeanPool.lean | Adds the new Polylean modules to the repository’s aggregate import file. |
Comments suppressed due to low confidence (2)
LeanPool/Polylean/UnitConjecture/GroupRing.lean:157
mul_zero_consuseshin((0, h) :: t)and latermul_monom_zero h ..., buthis not in scope (not a parameter and not introduced by the induction). This won’t compile; add(h : G)as an explicit argument or destructure the relevant head element and use itsGcomponent.
/-- multiplication equivalent when adding term with `0` coefficient -/
theorem mul_zero_cons (s t : FormalSum R G) : mul s ((0, h) :: t) ≈ mul s t := by
induction s
LeanPool/Polylean/UnitConjecture/FreeModule.lean:398
- In
beq_quot,eqv₁/eqv₂are equivalences for aQuotient(Setoid) lift, but the proof usesQuot.sound(forQuot). This should beQuotient.sound(or rewrite usingQuotient.eq/Quotient.sound) so the well-definedness proof compiles.
apply Quotient.lift₂
(fun (s₁ s₂ : FormalSum R X) => decide (@Eq (R[X]) ⟦s₁⟧ ⟦s₂⟧))
intro a₁ b₁ a₂ b₂ eqv₁ eqv₂
let eq₁ : Eq (α := R[X]) ⟦a₁⟧ ⟦a₂⟧ := Quot.sound eqv₁
let eq₂ : Eq (α := R[X]) ⟦b₁⟧ ⟦b₂⟧ := Quot.sound eqv₂
|
|
||
| -- associativity with two terms monomials | ||
| omit [DecidableEq R] in | ||
| theorem mul_monom_monom_assoc (a b : R) (h x₀ : G) |
|
|
||
| omit [DecidableEq R] in | ||
| /-- Associativity of scalar multiplication coordinates for a formal sum with one term. -/ | ||
| theorem monom_coords_mul (x₀ : X) (a b : R) : |
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | algebra |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
It formalizes Gardam's disproof of Kaplansky's Unit Conjecture by proving torsion-freeness of the Promislow group and verifying a nontrivial unit in its group ring over 𝔽₂.
Tokens: 64,699 in / 812 out · Tier: flex · Cost: $0.1739
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
Deterministic partial-port audit flags this PR as incomplete against the registered upstream source. Compared with That matches the LLM review concern: the current PR proves the torsion-freeness infrastructure, but not the actual Gardam theorem/counterexample layer from the upstream project. Treating this as request-changes until the missing upstream theorem file and its dependencies are ported, or the project card/source scope is explicitly narrowed. This is the failure mode automated in #110. |
|
/review |
|
LLM review skipped: Lean Action CI conclusion was |
|
/review |
|
Follow-up on the partial-port audit: this blocker is resolved on the current head. Commit |
|
/profile |
…-20260518-144229 # Conflicts: # LeanPool.lean # LeanPool/projects.yml
|
/review |
|
Follow-up after the full port cleanup: this PR now imports the previously missing clean Polylean modules, including Current head |
# Conflicts: # LeanPool.lean # LeanPool/projects.yml
|
Follow-up audit after the partial-port review: the Gardam theorem / Unit Conjecture result is present in the merged PR ( After #132, the only upstream Polylean files still not represented are:
|
Imported from https://github.com/siddhartha-gadgil/Polylean.
Slug:
polyleanToolchain target:
leanprover/lean4:v4.30.0-rc2Branch:
import/polylean-retry-20260518-144229(retry run20260518-144229)Agent:
codexusinggpt-5.5at effortxhigh.Commits on this branch:
Opened manually after
scripts/import-formalization.shfinished the agent run but exited before PR creation due to the running wrapper script seeingmainchange under it. The branch was rebased onto currentorigin/mainand checked for content-only diff before push.