Prime-factor statistics of p − 1 - Revision history

Aftermath bot: Follow-up: plasma-ai/erdos-408 (Erdos Problem 408 in Lean) builds on this result

2026-10-15T02:48:43Z

Follow-up: plasma-ai/erdos-408 (Erdos Problem 408 in Lean) builds on this result

← Older revision		Revision as of 19:48, 14 October 2026
Line 7:		Line 7:
	* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.		* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.
	* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''<sup>''c''</sup> infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.		* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''<sup>''c''</sup> infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
	* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).		* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 15 October 2026).

	== Public follow-up work ==		== Public follow-up work ==
	{\| class="wikitable"		{\| class="wikitable"
	! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)		! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
	\|-		\|-
	\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.		\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
Line 20:		Line 20:
	\|-		\|-
	\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) \|\| Formalization (Lean) \|\| A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''<sup>2−ε</sup> for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. \|\| Author-reported; the README states that the work was developed with AI assistance. An open Formal Conjectures pull request, [https://github.com/google-deepmind/formal-conjectures/pull/7315 #7315] (opened 14 October 2026), proposes marking the Formal Conjectures statement of Problem 824 as solved, with a link to release v1.0.0 of this repository.		\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) \|\| Formalization (Lean) \|\| A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''<sup>2−ε</sup> for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. \|\| Author-reported; the README states that the work was developed with AI assistance. An open Formal Conjectures pull request, [https://github.com/google-deepmind/formal-conjectures/pull/7315 #7315] (opened 14 October 2026), proposes marking the Formal Conjectures statement of Problem 824 as solved, with a link to release v1.0.0 of this repository.
			\|-
			\| 2026-10-14 \|\| [https://github.com/plasma-ai/erdos-408 plasma-ai/erdos-408] (GitHub, Plasma AI; paper in the repository, ''The normal order of the number of iterations of Euler's function'') \|\| Use (Lean) \|\| A Lean project claiming an unconditional answer to the first two questions of Erdős Problem 408: writing ''f''(''n'') for the number of iterations of φ needed to reach 1, ''f''(''n'')/log ''n'' tends to a constant α with 1/log 3 ≤ α ≤ 1/log 2 on a set of density one, with a mean-square rate. The README states that the argument extends results of the Poisson–Dirichlet and weighted-dilation-graph manuscripts of this family (with Lean proofs of the extensions), uses a vendored Lean formalization of the latter by Yao Xu, and takes the zero-free half-plane of [[The quasi-Riemann hypothesis]] as a vendored Lean input; its Comparator configuration permits only the three standard axioms. The formal statements of parts (i) and (ii) are copied from formal-conjectures. \|\| Public repository; review status "self-assessed".
	\|}		\|}

Aftermath bot: Add open Formal Conjectures pull requests for Problems 821 and 824

2026-10-14T19:53:27Z

Add open Formal Conjectures pull requests for Problems 821 and 824

← Older revision		Revision as of 12:53, 14 October 2026
Line 17:		Line 17:
	\| 2026-10-11 \|\| S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824], Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000021&version=1 PALOMAR-2026-10-11-000021], version 1) \|\| Use (conditional) \|\| Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''<sup>2−o(1)</sup>, conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. \|\| arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.		\| 2026-10-11 \|\| S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824], Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000021&version=1 PALOMAR-2026-10-11-000021], version 1) \|\| Use (conditional) \|\| Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''<sup>2−o(1)</sup>, conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. \|\| arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.
	\|-		\|-
	\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance.		\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance. An open Formal Conjectures pull request, [https://github.com/google-deepmind/formal-conjectures/pull/7314 #7314] (opened 14 October 2026), proposes marking the Formal Conjectures statement of Problem 821 as solved, with a link to release v1.0.0 of this repository.
	\|-		\|-
	\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) \|\| Formalization (Lean) \|\| A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''<sup>2−ε</sup> for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. \|\| Author-reported; the README states that the work was developed with AI assistance.		\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) \|\| Formalization (Lean) \|\| A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''<sup>2−ε</sup> for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. \|\| Author-reported; the README states that the work was developed with AI assistance. An open Formal Conjectures pull request, [https://github.com/google-deepmind/formal-conjectures/pull/7315 #7315] (opened 14 October 2026), proposes marking the Formal Conjectures statement of Problem 824 as solved, with a link to release v1.0.0 of this repository.
	\|}		\|}

Aftermath bot: Add the Lean proof of Erdős 824 (cadamcat/equal-divisor-sums-lean4) and the Palomar link for Li–Zhuang

2026-10-14T05:07:14Z

Add the Lean proof of Erdős 824 (cadamcat/equal-divisor-sums-lean4) and the Palomar link for Li–Zhuang

← Older revision		Revision as of 22:07, 13 October 2026
Line 15:		Line 15:
	\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.		\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
	\|-		\|-
	\| 2026-10-11 \|\| S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824]) \|\| Use (conditional) \|\| Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''<sup>2−o(1)</sup>, conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. \|\| arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.		\| 2026-10-11 \|\| S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824], Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000021&version=1 PALOMAR-2026-10-11-000021], version 1) \|\| Use (conditional) \|\| Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''<sup>2−o(1)</sup>, conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. \|\| arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.
	\|-		\|-
	\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance.		\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance.
			\|-
			\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/equal-divisor-sums-lean4 cadamcat/equal-divisor-sums-lean4] (GitHub; commit <code>6280393</code>) \|\| Formalization (Lean) \|\| A Lean 4 proof of Erdős Problem 824: for every ε > 0, the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') exceeds ''x''<sup>2−ε</sup> for all large ''x'', with the target statement following the Formal Conjectures statement of the problem. The README describes the route as Li and Zhuang's conditional theorem combined with the successor form of the totient-fibre manuscript's smooth-shifted-prime theorem (primes ''p'' = 2''u'' − 1 with ''p'' + 1 smooth), built on the Erdős 821 formalization above; it states that the proofs are verified by the Lean 4 kernel and describes the same kind of verification script. \|\| Author-reported; the README states that the work was developed with AI assistance.
	\|}		\|}

Aftermath bot: Add arXiv follow-ups (Banks, Pintz–Althöfer, Sang, Frei–Sofos–Widmer; Li–Zhuang; Li–Su)

2026-10-14T04:47:14Z

Add arXiv follow-ups (Banks, Pintz–Althöfer, Sang, Frei–Sofos–Widmer; Li–Zhuang; Li–Su)

← Older revision		Revision as of 21:47, 13 October 2026
Line 14:		Line 14:
	\|-		\|-
	\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.		\| 2026-10-08 \|\| J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 \|\| Use (conditional consequence) \|\| Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''<sup>5/12−ε</sup>, and ''x''<sup>0.4736−ε</sup> with Harman's admissible value) and for Novak–Carmichael numbers (''x''<sup>1−o(1)</sup>). \|\| The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
			\|-
			\| 2026-10-11 \|\| S. Li, Z. Zhuang, ''Coprime pairs with equal sum of divisors, assuming smooth shifted primes'' ([https://arxiv.org/abs/2610.15674 arXiv:2610.15674], v1; Lean code at [https://github.com/daizisheng/erdos-824 daizisheng/erdos-824]) \|\| Use (conditional) \|\| Erdős Problem 824: the number of coprime pairs ''a'' < ''b'' < ''x'' with σ(''a'') = σ(''b'') is ''x''<sup>2−o(1)</sup>, conditionally on the correctness of the totient-fibre manuscript, whose argument for smooth values of ''p'' − 1 the authors check transfers to ''p'' + 1 after a change of sign in two of its sections. The implication from smooth shifted primes, an argument of Pollack and Pomerance, is written out with explicit parameters and formalized in Lean 4. \|\| arXiv v1. The abstract states that the manuscript has not been refereed and that the authors have not independently verified its main new estimates.
	\|-		\|-
	\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance.		\| 2026-10-14 \|\| Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) \|\| Formalization (Lean) \|\| A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. \|\| Author-reported; the README states that the work was developed with AI assistance.

Aftermath bot: New page: prime-factor statistics of p − 1 (openai/math 011) with two public follow-ups; Main Page link

2026-10-14T02:55:43Z

New page: prime-factor statistics of p − 1 (openai/math 011) with two public follow-ups; Main Page link

New page

'''Prime-factor statistics of p − 1''' is a family of three manuscripts dated September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). They concern the prime factors of the predecessor ''p'' − 1 of a prime ''p'', and one of them addresses Erdős's conjecture on the largest fibres of Euler's totient function (Erdős Problem #821). This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original results ==
* '''Totient fibres and smooth shifted primes.''' For every ε > 0, infinitely many positive integers ''n'' have more than ''n''1−ε solutions ''m'' of φ(''m'') = ''n''. The arithmetic input is that, for every fixed 0 < δ < 1/4, at least ''x''1−o(1) primes ''p'' with 2''x'' < ''p'' ≤ 5''x'' have every prime factor of ''p'' − 1 at most ''x''δ; the manuscript notes that the count also holds for every fixed δ > 0. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weighted-Dilation-Graphs-Smooth-Shifted-Primes-and-Totient-Fibers-September-24-2026 ''Weighted dilation graphs, smooth shifted primes and totient fibers''] (24 September 2026).
* '''Poisson–Dirichlet law.''' For a prime ''p'' chosen uniformly from 3 ≤ ''p'' ≤ ''x'', the logarithms of the prime factors of ''p'' − 1 (in decreasing order, with multiplicity), divided by log(''p'' − 1), converge in every finite joint distribution to the Poisson–Dirichlet distribution with parameter one. The manuscript states that this proves a conjecture of Ford, Konyagin and Luca. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Poisson-Dirichlet-Law-for-Prime-Predecessors-September-24-2026 ''The Poisson-Dirichlet law for prime predecessors''] (24 September 2026).
* '''Even number of prime factors.''' There are infinitely many primes ''p'' for which ''p'' − 1 is squarefree with an even number of prime factors, that is, μ(''p'' − 1) = 1. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Prime-Predecessors-with-an-Even-Number-of-Prime-Factors-September-17-2026 ''Prime predecessors with an even number of prime factors''] (17 September 2026).
* '''Formalization.''' The collection's index (commit <code>adc7f12</code>) lists no Lean formalization for this family.
* '''Earlier results, as summarized in the totient-fibre manuscript.''' Pomerance (1980) formulated the conjecture as ''C'' = 1, where ''C'' is the supremum of exponents ''c'' with ''g''(''n'') > ''n''''c'' infinitely often, and attributed it to Erdős. Baker and Harman (1998) obtained smoothness exponent 0.2961 for shifted primes and totient multiplicity exponent 0.7039. Lichtman (2022) proved a lower bound for every smoothness exponent above 15/(32√e) = 0.2843… and obtained multiplicity exponent 0.7156. Bharadwaj and Rodgers (2026) prove the full Poisson–Dirichlet law for shifted primes under the Elliott–Halberstam conjecture.
* '''Problem database.''' The erdosproblems.com entry for [https://www.erdosproblems.com/821 Problem 821] (page last edited 1 October 2025) records Lichtman's exponent 0.71568… as the best known bound (checked 14 October 2026).

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || J. Guo, [https://github.com/aster2024/openai-math-followups aster2024/openai-math-followups] (GitHub), consequences list, item 2 || Use (conditional consequence) || Conditional on Theorem 1.1 of the Poisson–Dirichlet manuscript, and through results of Alford, Granville and Pomerance and of Kalmynin, lower bounds for the counts of Carmichael numbers (''x''5/12−ε, and ''x''0.4736−ε with Harman's admissible value) and for Novak–Carmichael numbers (''x''1−o(1)). || The repository states that the list was compiled with AI systems under the author's direction and that the author takes responsibility for its content.
|-
| 2026-10-14 || Yao Xu, [https://github.com/cadamcat/totient-fibers-lean4 cadamcat/totient-fibers-lean4] (GitHub; commit <code>dfce357</code>) || Formalization (Lean) || A Lean 4 formalization of Erdős Problem 821 that follows the totient-fibre manuscript, with its target statement aligned to the Formal Conjectures statement of the problem. The README states that the proofs are verified by the Lean 4 kernel and describes a verification script that compares the statement, scans for forbidden constructs and checks the axioms used. || Author-reported; the README states that the work was developed with AI assistance.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]