Skip to content

Conversation

@saumilyagupta
Copy link
Contributor

This file introduces Green's Open Problem 100, discussing whether every group is well-approximated by finite groups and defining the concept of residual finiteness.

closes: #1756

Reference: https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.100

This file introduces Green's Open Problem 100, discussing whether every group is well-approximated by finite groups and defining the concept of residual finiteness. 
closes: google-deepmind#1756
@github-actions github-actions bot added the green-problems Problems from https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf label Jan 22, 2026
@YaelDillies YaelDillies changed the title Add Green's Open Problem 100 definition and theorem feat(GreensOpenProblems): 100 Jan 22, 2026
@YaelDillies YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 22, 2026
saumilyagupta and others added 2 commits January 22, 2026 22:13
Co-authored-by: Sachit Ramesh <sachit.rg17@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Comment on lines +35 to +37
Equivalently, is every group residually finite? A group $G$ is residually finite if for every
non-identity element $g \in G$, there exists a normal subgroup $N$ such that $G/N$ is finite
and $g \notin N$.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Where did you get this equivalence from? I can't find it in the PDF

Copy link
Member

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you using AI to avoid having to understand the conjecture yourself? Such behavior is wasting everyone's time and will get you banned from this repo.

Comment on lines +41 to +43
answer(sorry) ↔
∀ (G : Type) [Group G],
(∀ (g : G), g ≠ 1 → ∃ (N : Subgroup G), N.Normal ∧ Finite (G ⧸ N) ∧ g ∉ N) := by
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is certainly false. Consider G to be the rationals

@saumilyagupta
Copy link
Contributor Author

Are you using AI to avoid having to understand the conjecture yourself? Such behavior is wasting everyone's time and will get you banned from this repo.

I am using AI to help me understand the problem and write the code properly.
However, I did not check the details thoroughly, and that was my mistake. I sincerely apologize, and I will make sure this does not happen again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author The author should answer a question or perform changes. Reply when done. green-problems Problems from https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Green's Open Problems #100

3 participants