Skip to content

Commit ddf9296

Browse files
Updated Dickson's conjecture references and wording (#3655)
## Summary Refresh the references and wording in the existing Dickson's conjecture formalization. ## Context Issue #3627 asks for a formalization of Dickson's conjecture, but the conjecture is already present in the repository as `Dickson.dickson_conjecture` in `FormalConjectures/Wikipedia/Dickson.lean`. This PR does not add a new theorem. Instead, it makes a small cleanup to the existing file by: - adding source links that match the issue references - fixing a docstring wording typo ## Existing implementation The conjecture is already formalized here: - `FormalConjectures/Wikipedia/Dickson.lean` - theorem: `Dickson.dickson_conjecture` The existing theorem predates the issue: - core theorem lines trace back to commit `bf6aef2` from 2025-06-23 - issue #3627 was opened on 2026-03-24 ## Changed file - `FormalConjectures/Wikipedia/Dickson.lean` ## What changed - added PrimePages, OEIS Wiki, MathWorld, and Dickson book references - corrected the docstring text from `a finite set of in linear integer forms` to `a finite set of linear integer forms` ## Review notes This PR is intentionally small. Its main value is to make the existing implementation easier to match against issue #3627, which appears to already be solved by the current repository state. Closes #3627
1 parent ba88589 commit ddf9296

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

FormalConjectures/Wikipedia/Dickson.lean

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,14 +22,18 @@ open Polynomial
2222
2323
*References:*
2424
- [Wikipedia](https://en.wikipedia.org/wiki/Dickson%27s_conjecture)
25+
- [PrimePages glossary](https://t5k.org/glossary/xpage/DicksonsConjecture.html)
26+
- [OEIS Wiki](https://oeis.org/wiki/Dickson%27s_conjecture)
27+
- [MathWorld](https://mathworld.wolfram.com/DicksonsConjecture.html)
28+
- [Leonard Eugene Dickson, *History of the Theory of Numbers, Vol. I: Divisibility and Primality*](https://archive.org/details/historyoftheoryo01dickuoft)
2529
- [Arxiv](https://arxiv.org/pdf/0906.3850)
2630
-/
2731

2832
namespace Dickson
2933

3034
/--
3135
**Dickson's conjecture**
32-
If a finite set of in linear integer forms $f_i(n) = a_i n+b_i$ satisfies Schinzel condition,
36+
If a finite set of linear integer forms $f_i(n) = a_i n+b_i$ satisfies Schinzel condition,
3337
there exist infinitely many natural numbers $m$ such that $f_i(m)$ are primes for all $i$.
3438
-/
3539
@[category research open, AMS 11]

0 commit comments

Comments
 (0)