Skip to content

feat(NumberTheory): Green-Tao theorem#222

Open
thomaskwaring wants to merge 7 commits into
leanprover:mainfrom
thomaskwaring:green-tao
Open

feat(NumberTheory): Green-Tao theorem#222
thomaskwaring wants to merge 7 commits into
leanprover:mainfrom
thomaskwaring:green-tao

Conversation

@thomaskwaring
Copy link
Copy Markdown

There are arbitrarily long arithmetic progressions of primes.

Comment thread LeanEval/NumberTheory/GreenTao.lean Outdated
Comment thread LeanEval/NumberTheory/GreenTao.lean Outdated
Comment thread manifests/problems.toml Outdated
twwar and others added 3 commits May 15, 2026 10:16
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Ben Green and Terence Tao. *The primes contain arbitrarily long arithmetic progressions* (2004).
-/

/-- The *Green-Tao Theorem*: there are arbitrarily long arithmetic progressions of primes. -/
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Suggested change
/-- The *Green-Tao Theorem*: there are arbitrarily long arithmetic progressions of primes. -/
/-- The *GreenTao Theorem*: there are arbitrarily long arithmetic progressions of primes. -/

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants