partial-regularity/formalization.yaml at main · AxiomMath/partial-regularity · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json

version: "v0.4"

project:
  name: "PartialRegularity"
  authors: [Kenny Lau]
  description: >
    `PartialRegularity` is a formal proof of the main theorem of *Almost all primes are partially
    regular* (arXiv:2602.05090): for fixed $\alpha > 1/2$, the number of primes $p \le X$ that are
    not $M_\alpha(p)$-regular is $O(X/(\log X)^{2\alpha})$ as $X \to +\infty$. The Lean files were
    generated by AxiomProver, Axiom Math's in-house theorem proving system.
  responsible_maintainers: [Kenny Lau]
  license: "MIT"

repository:
  role: "substantive-development"

sources:
  - title: "Almost all primes are partially regular"
    authors: [Evan Chen, Chris Cummins, Ben Eltschig, Dejan Grubisic, Leopold Haller, Letong Hong, Andranik Kurghinyan, Kenny Lau, Hugh Leather, Seewoo Lee, Aram Markosyan, Ken Ono, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Shubho Sengupta, Ishan Sinha, Jimmy Xin, Jujian Zhang]
    id: "https://arxiv.org/abs/2602.05090"
    type: "article"
    location: "Theorem 1.1"
    relationship: "formalizes"
    note: >
      Formalized twice, in two problem/solution pairs: the main run and a second run given
      additional tools, whose files are under `extension/`.

classification:
  arxiv: [math.NT]
  msc2020: [11Y40, 11R18]

status:
  scope: >
    Theorem 1.1 for every $\alpha > 1/2$. The bound is stated as an `IsBigO` relation along
    `atTop` rather than with the explicit constant $C_\alpha$ of the paper. The main run counts
    primes $p \le X$ over real $X$ with a `Finset` filter; the `extension` run counts odd primes
    over natural $X$ with a `Set`.
  sorry_count: 0
  sorry_in_definitions: 0
  axioms: [propext, Quot.sound, Classical.choice]
  main_results:
  - declaration: "irregular_primes_asymptotic"
    file: "PartialRegularity/solution.lean"
    sorry_count: 0
    axioms: [propext, Quot.sound, Classical.choice]
    comparator_config: "comparator.json"
  - declaration: "irregularPrimes_isBigO"
    file: "extension/ext_solution.lean"
    sorry_count: 0
    axioms: [propext, Quot.sound, Classical.choice]
    comparator_config: "comparator-extension.json"

automation:
  methods:
    - method: "autonomous"
      models: [AxiomProver]

review:
  status: "author-verified"
  reviewers: [Kenny Lau]
  notes: >
    The formal challenge in `PartialRegularity/problem.lean` and `extension/ext_problem.lean` was
    checked against the source paper by an author of that paper.

alignment:
  statements:
    - source: "Almost all primes are partially regular (Theorem 1.1)"
      lean: "irregular_primes_asymptotic"
      module: "PartialRegularity.solution"
      status: "Proved, as an `IsBigO` relation rather than with an explicit $C_\\alpha$."
    - source: "Almost all primes are partially regular (Theorem 1.1)"
      lean: "irregularPrimes_isBigO"
      module: "extension.ext_solution"
      status: "Proved, in the `extension` run, over odd primes indexed by natural $X$."