Import the finitely presented non-sofic group proof - #385
Open
Vilin97 wants to merge 10 commits into
Open
Conversation
Greptile SummaryThe PR imports a formalization proving the existence of a finitely presented non-sofic group and registers its public headline result.
|
| Filename | Overview |
|---|---|
| LeanPool/NonSoficGroup.lean | Defines the project entry module and identifies the finitely presented non-sofic group theorem as its headline result. |
| LeanPool/NonSoficGroup/Foundations.lean | Introduces the foundational definitions and constructions used by the non-sofic group proof. |
| LeanPool/NonSoficGroup/Spectral.lean | Adds the spectral and finite-approximation arguments consumed by the compression layer. |
| LeanPool/NonSoficGroup/Compression.lean | Adds the rooted-model and component-compression arguments used in the final contradiction. |
| LeanPool/NonSoficGroup/Conclusion.lean | Completes the proof and exposes the existential theorem matching the advertised headline. |
| LeanPool/projects.yml | Registers the project, its mixed provenance, pinned upstream source, and headline declaration. |
| LeanPool.lean | Adds the new project and implementation modules to the repository-wide import surface. |
Reviews (8): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
Contributor
Proof profile (new / modified Lean files)
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: 8,417 maxHeartbeats units across 5 files (35,296 added LOC). Sum of Count-heartbeats wall-clock total: 180.81 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.NonSoficGroup.Foundations |
48.00 s |
LeanPool.NonSoficGroup.Spectral |
33.00 s |
LeanPool.NonSoficGroup.Compression |
20.00 s |
LeanPool.NonSoficGroup.Conclusion |
12.00 s |
LeanPool.NonSoficGroup |
1.20 s |
Per-file `lean --profile` output
LeanPool/NonSoficGroup.lean
import took 4.31s
cumulative profiling times:
elaboration 0.184ms
import 4.31s
initialization 36.7ms
interpretation 167ms
linting 0.277ms
module linting 0.00188ms
overlappingInstancesLinter 0.332ms
parsing 0.0321ms
tacticAnalysis 2.68ms
real 5.03
user 1.12
sys 0.62
LeanPool/NonSoficGroup/Compression.lean
import took 3.49s
simp took 166ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 108ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 443ms
interpretation of Mathlib.Meta.Positivity.evalMul._lam_3._boxed took 118ms
type checking took 201ms
type checking took 184ms
type checking took 176ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 104ms
type checking took 226ms
type checking took 210ms
type checking took 241ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 272ms
simp took 150ms
cumulative profiling times:
aesop 21ms
attribute application 3.33ms
blocked (unaccounted) 0.656ms
compilation (IR) 1.72ms
compilation (LCNF base) 23.1ms
compilation (LCNF impure) 6.92ms
compilation (LCNF mono) 14.2ms
congr simp thm 132ms
dsimp 60.3ms
elaboration 2.86s
fix level params 62.4ms
grind 78ms
grind mark subsingleton 5.59ms
grind simp 22ms
import 3.49s
initialization 38.6ms
instantiate metavars 80.2ms
interpretation 10.6s
let-to-have transformation 13.4ms
linting 923ms
module linting 0.00164ms
norm_num 644ms
overlappingInstancesLinter 143ms
parsing 538ms
process pre-definitions 373ms
ring 622ms
share common exprs 313ms
simp 4.44s
sym canon 9.59ms
sym typeclass inference 215ms
tactic execution 7.97s
tacticAnalysis 1.15s
type checking 3.19s
typeclass inference 14.1s
real 18.05
user 49.62
sys 1.04
LeanPool/NonSoficGroup/Conclusion.lean
import took 1.25s
elaboration took 106ms
type checking took 288ms
elaboration took 125ms
tactic execution of Lean.Parser.Tactic.obtain took 306ms
tactic execution of Lean.Parser.Tactic.obtain took 662ms
elaboration took 202ms
tactic execution of Lean.Parser.Tactic.refine took 154ms
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 159ms
interpretation of Mathlib.Meta.Positivity.evalDiv._lam_0._boxed took 106ms
elaboration took 114ms
tactic execution of Lean.Parser.Tactic.obtain took 198ms
cumulative profiling times:
attribute application 1.84ms
compilation (IR) 1.72ms
compilation (LCNF base) 36.8ms
compilation (LCNF impure) 7.32ms
compilation (LCNF mono) 19.9ms
congr simp thm 85.6ms
dsimp 89.4ms
elaboration 2.92s
fix level params 26.3ms
import 1.25s
initialization 33.5ms
instantiate metavars 92.5ms
interpretation 4.32s
let-to-have transformation 12.5ms
linting 514ms
module linting 0.00183ms
norm_num 84.3ms
overlappingInstancesLinter 69.6ms
parsing 291ms
process pre-definitions 204ms
ring 87.3ms
share common exprs 169ms
simp 2.92s
tactic execution 7.26s
tacticAnalysis 645ms
type checking 1.55s
typeclass inference 7.88s
real 9.73
user 30.47
sys 0.82
LeanPool/NonSoficGroup/Foundations.lean
import took 1.21s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 208ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 443ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 319ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 263ms
elaboration took 692ms
simp took 593ms
simp took 510ms
simp took 984ms
tactic execution of Lean.Parser.Tactic.simp took 160ms
tactic execution of Lean.Parser.Tactic.decide took 270ms
type checking took 121ms
simp took 3.39s
tactic execution of Lean.Parser.Tactic.simp took 250ms
simp took 518ms
type checking took 137ms
simp took 535ms
tactic execution of Lean.Parser.Tactic.simp took 440ms
simp took 541ms
simp took 541ms
simp took 546ms
simp took 566ms
simp took 597ms
simp took 602ms
simp took 631ms
simp took 641ms
simp took 641ms
simp took 550ms
simp took 581ms
simp took 526ms
simp took 422ms
simp took 430ms
simp took 440ms
simp took 457ms
simp took 461ms
simp took 481ms
type checking took 358ms
simp took 273ms
simp took 136ms
simp took 692ms
typeclass inference of AddHomClass took 102ms
cumulative profiling times:
aesop 180ms
attribute application 17.6ms
blocked (unaccounted) 15.1s
compilation (IR) 17.1ms
compilation (LCNF base) 383ms
compilation (LCNF impure) 70.6ms
compilation (LCNF mono) 192ms
congr simp thm 186ms
dsimp 100ms
elaboration 4.11s
fix level params 79.9ms
import 1.21s
initialization 36.9ms
instantiate metavars 124ms
interpretation 11.1s
let-to-have transformation 17.9ms
linting 1.06s
module linting 0.00194ms
norm_num 640ms
overlappingInstancesLinter 247ms
parsing 629ms
process pre-definitions 686ms
ring 515ms
share common exprs 450ms
simp 23s
tactic execution 10.6s
tacticAnalysis 1.41s
type checking 4.36s
typeclass inference 16.2s
real 27.45
user 77.27
sys 1.45
LeanPool/NonSoficGroup/Spectral.lean
import took 1.27s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 262ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 348ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 360ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 927ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 119ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 862ms
tactic execution of Lean.Parser.Tactic.exact took 221ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 165ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 349ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 177ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 181ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 189ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 193ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 196ms
tactic execution of Mathlib.Tactic.nlinarith took 142ms
typeclass inference of MulOne took 104ms
typeclass inference of MulOneClass took 108ms
typeclass inference of MulOne took 102ms
typeclass inference of NonUnitalNonAssocSemiring took 150ms
tactic execution of Lean.Parser.Tactic.change took 101ms
typeclass inference of MulOneClass took 111ms
typeclass inference of MulOneClass took 102ms
typeclass inference of MulHomClass took 108ms
typeclass inference of MulOne took 106ms
tactic execution of Lean.Parser.Tactic.omega took 159ms
type checking took 134ms
simp took 118ms
simp took 137ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 359ms
tactic execution of Mathlib.Tactic.nlinarith took 489ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 289ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 328ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 434ms
tactic execution of Lean.Parser.Tactic.exact took 143ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 281ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 250ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 469ms
simp took 133ms
tactic execution of Mathlib.Tactic.nlinarith took 141ms
simp took 227ms
simp took 178ms
simp took 227ms
simp took 177ms
simp took 173ms
simp took 170ms
cumulative profiling times:
aesop 219ms
attribute application 24.3ms
blocked (unaccounted) 3.76s
compilation (IR) 4.89ms
compilation (LCNF base) 59.9ms
compilation (LCNF impure) 19.1ms
compilation (LCNF mono) 48.8ms
congr simp thm 220ms
dsimp 123ms
elaboration 4.59s
fix level params 126ms
import 1.27s
initialization 33.1ms
instantiate metavars 142ms
interpretation 16.5s
let-to-have transformation 30.4ms
linting 1.2s
module linting 0.00178ms
norm_num 816ms
overlappingInstancesLinter 273ms
parsing 649ms
process pre-definitions 681ms
ring 754ms
share common exprs 494ms
simp 7.51s
tactic execution 12.8s
tacticAnalysis 1.44s
type checking 5.01s
typeclass inference 33.9s
real 26.64
user 88.60
sys 1.34
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
The headline declaration exactly proves the existence of a finitely presented group that is not sofic. |
| Novelty | ✅ pass |
The headline is not already formalized in the reported Mathlib search or the pool project list. |
| Significance | ✅ pass |
The PR proves a major research-level headline result and is a clear fit for the pool. |
| Sources | ✅ pass |
The cited upstream formalization and optimization provenance are internally consistent with the claimed result, but the source contents cannot be independently verified from the diff. |
| Code quality (advisory) | 🤔 discuss |
A human should consolidate the parallel APIs and repeated generic proofs and trim the import residue before treating this development as maintainable. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | geometric and combinatorial group theory |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The theorem produces G : Type with a group structure and proves Group.IsFinitelyPresented G ∧ ¬ Sofic G, matching the card’s informal statement.
The contribution is a formal proof that a finitely presented non-sofic group exists, resolving the question whether every group is sofic.
Code quality findings (4)
- import-residue —
LeanPool/NonSoficGroup/Foundations.lean:30
The foundations module imports several subject-specific libraries and tactic plugins with no corresponding use in the diff, increasing the dependency surface and exposing this project to unrelated changes. Remove the unused height theory, totally split, sheaf, specializedNormNum, andBVDecideimports individually.
Evidence: The import block includes:
import Mathlib.NumberTheory.Height.NumberField
import Mathlib.NumberTheory.Height.Projectivization
import Mathlib.RingTheory.TotallySplit
import Mathlib.Tactic.NormNum.LegendreSymbol
import Mathlib.Tactic.NormNum.NatFib
import Mathlib.Tactic.NormNum.Ordinal
import Mathlib.Topology.Sheaves.Init
import Std.Tactic.BVDecide.Normalize.Prop
No declarations or tactics in the added files use the APIs specific to these modules. - duplicate-definition — PR-wide
The PR defines the same domain objects repeatedly under different namespaces, then adds bridge equalities and largesimpalists to move between them. Use one canonical indicator, real Markov operator, source inclusion, compression table, and real-variation definition; make any conceptual names abbreviations rather than independent definitions. The repeated pairs includeKunDirectedIndicatorJensen.realIndicator/KunFinitePermutationMarkovMass.realIndicator/KunActualRootedModelBridge.sourceFiniteIndicator, four versions of the real Markov operator,SourceGeneratedWordCrossing.sourceAlphaInclusion/KunExactActualSourceAmbientGenerators.sourceAlphaInclusion, bothsourceCompressionTabledefinitions, and bothpermutationRealVariationdefinitions.
Evidence: Both indicator namespaces contain the identical body:
public
def realIndicator {V : Type*} [DecidableEq V]
(T : Finset V) (x : V) : ℝ :=
if x ∈ T then 1 else 0
The duplication requires explicit bridges such as:
private theorem rooted_realMarkov_eq_mass_realPermutationMarkov
{ι V : Type*} [Fintype ι]
(p : ι → Equiv.Perm V) :
KunRealComplexMarkovBridge.realMarkov p =
KunFinitePermutationMarkovMass.realPermutationMarkov p := by
The source inclusion is also repeated verbatim:
public
def sourceAlphaInclusion :
prefixElementaryGroup alphaPrefixCode →*
prefixElementaryGroup ninePrefixCode where
toFun g :=
⟨g.val,
SourceGeneration.alphaPrefixElementaryGroup_le_nine
g.property⟩
map_one' := rfl
map_mul' _ _ := rfl
- duplicate-lemma — PR-wide
Generic utilities are re-proved in multiple namespaces instead of being shared. Consolidate the three symmetric-generator word existence proofs, the repeated action-list-product and action-inverse convergence proofs, the partition-intersection sum, and the duplicatesourceCompletionBadsubset proof in a common internal module. The current copies can silently diverge when one proof or interface changes.
Evidence: Foundations contains the same partition identity twice:
public
theorem sum_card_inter_partition {α : Type*} [DecidableEq α]
{U : Finset α} (P : Finpartition U) (B : Finset α) :
∑ C ∈ P.parts, (C ∩ B).card = (U ∩ B).card := by
public
theorem matched_sum_card_inter_partition
{V : Type*} [DecidableEq V] {U : Finset V}
(P : Finpartition U) (B : Finset V) :
∑ C ∈ P.parts, (C ∩ B).card = (U ∩ B).card := by
The same closure-induction construction appears as exists_word_of_symmetric_generators, exists_word_of_symmetric_generating_finset, and exists_generator_word_of_symmetric_generates. The inverse-action convergence argument appears as tendsto_action_inverse and twice as sofic_action_inverse_normalizedHamming_tendsto_zero. MatchedComponentCompletion.sourceCompletionBad_subset is later duplicated as MatchedComponentExitBudget.sourceCompletionBad_subset_survivors.
- agent-slop — PR-wide
Elementary indicator obligations are repeatedly expanded into nested case splits and impossible-branch eliminations. Replace these blocks with direct normalization after one membership split; the same issue occurs insourceRootedIndicatorMarkovModel_isGenerated,completedGoodPermutationGraphRootedModel_isGenerated, and the indicator argument insideexists_source_sparse_cut_at_radius.
Evidence: One representative block is:
· intro x
change sourceFiniteIndicator T x = 0 ∨
sourceFiniteIndicator T x = 1
by_cases hx : x ∈ T
· right
unfold sourceFiniteIndicator
split
· rfl
· rename_i hnot
exact (hnot hx).elim
· left
unfold sourceFiniteIndicator
split
· rename_i hmem
exact (hx hmem).elim
· rfl
This can be discharged directly afterby_cases hx : x ∈ Tby simplifyingsourceFiniteIndicatorwithhx.
Tokens: 2,501,528 in / 12,666 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $12.7926
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.
Owner
Author
|
/review |
Contributor
|
LLM review skipped: Lean Action CI conclusion was |
Vilin97
added
the
needs-maintainer
Owner
Author
|
Automation disposition: needs-maintainer Reviewed exact head bda61ce after a verified repair pass. The card now faithfully describes the two-stage construction, dependency residue was replaced with precise imports, and the project builds. The remaining duplicated sourceAlphaInclusion, realIndicator, partition, and generator-word APIs are cross-module architecture work; quality remains below 4/5. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
94bc0fe, using Dean Cureton’s optimized proof at30c21d7.SoficGroups.exists_finitelyPresented_nonsofic_group.Optimization
Validation
lake build LeanPool.NonSoficGrouplake exe runLinteron the entry module and all four leaveslake exe lint-styleon the entry module and all four leaveslake exe mk_all --check#print axiomsaudit of all 319 exposed declarations: zero errors