Skip to content

Import the finitely presented non-sofic group proof #385

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 10 commits into
base: main
Choose a base branch
from
Open

Import the finitely presented non-sofic group proof #385

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
4e169e4
Import optimized non-sofic group proof core
Vilin97 Sep 4, 2026
48c82e6
Finalize optimized non-sofic group import
Vilin97 Sep 4, 2026
98f4ac7
Compile non-sofic internals privately
Vilin97 Sep 4, 2026
e198c52
fix: avoid Selberg sieve import collision
Vilin97 Sep 4, 2026
bda61ce
Tighten non-sofic dependencies and summary
Vilin97 Sep 4, 2026
1bf721f
Merge remote-tracking branch 'origin/main' into pr-385
github-actions[bot] Sep 4, 2026
e8ef41a
Merge remote-tracking branch 'origin/main' into pr-385
github-actions[bot] Sep 4, 2026
33712fa
Merge remote-tracking branch 'origin/main' into pr-385
github-actions[bot] Sep 4, 2026
76e494c
Merge remote-tracking branch 'origin/main' into pr-385
github-actions[bot] Sep 4, 2026
4c1ca08
Merge remote-tracking branch 'origin/main' into pr-385
github-actions[bot] Sep 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3040,6 +3040,11 @@ import LeanPool.MulticolorTriangleRamsey
import LeanPool.Neukirch
import LeanPool.Neukirch.ExtensionOfDedekindDomains
import LeanPool.Neukirch.HilbertRamificationTheory
import LeanPool.NonSoficGroup
import LeanPool.NonSoficGroup.Compression
import LeanPool.NonSoficGroup.Conclusion
import LeanPool.NonSoficGroup.Foundations
import LeanPool.NonSoficGroup.Spectral
import LeanPool.OSforGFF
import LeanPool.OSforGFF.Bochner
import LeanPool.OSforGFF.Bochner.FejerPD
Expand Down
21 changes: 21 additions & 0 deletions LeanPool/NonSoficGroup.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
/-
Copyright (c) 2026 OpenAI and Dean Cureton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: OpenAI, Dean Cureton
-/

module

public import LeanPool.NonSoficGroup.Foundations
public import LeanPool.NonSoficGroup.Conclusion

/-!
# Existence of a finitely presented non-sofic group

Source: url:https://github.com/openai/ten-proofs
Authors: OpenAI, Dean Cureton
Status: verified
Main declarations: `SoficGroups.exists_finitelyPresented_nonsofic_group`
Tags: group-theory, sofic-groups, property-t, finite-approximations
MSC: 20F65, 20E22
-/
Loading
Loading