Skip to content

feat(NumberTheory/AKSPrimality): Adds the AKS primality test#34507

Open
metakunt wants to merge 65 commits intoleanprover-community:masterfrom
metakunt:aks-introspective
Open

feat(NumberTheory/AKSPrimality): Adds the AKS primality test#34507
metakunt wants to merge 65 commits intoleanprover-community:masterfrom
metakunt:aks-introspective

Conversation

@metakunt
Copy link
Copy Markdown
Collaborator

@metakunt metakunt commented Jan 28, 2026 •
edited
Loading

Adds the completed proof for the AKS primality test.
Everything except the final theorem is marked private as it's only needed for the final proof.

Also everything except the final theorem is namespaced with AKS.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Aks.20primality.20Theorem.206.2E1.20Claim.20.28i.29.20proven

@github-actions github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Jan 28, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 28, 2026 •
edited
Loading

PR summary 06a46dae32

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.AKSPrimality (new file) 2502

Declarations diff

+ Conditions
+ Introspective
+ X_sub_C
+ aux
+ div
+ eval_pow
+ f
+ forall_in_se1_in_image_sp1_introspective
+ injective_f
+ injective_sp1
+ le_pow_floor_sqrt_se2
+ lt_sp2
+ mul_of_coprime
+ mul_poly
+ natDegree_le
+ of_multiset
+ one
+ pow_2_lt_choose
+ se1
+ se2
+ se2_choose_le_sp2
+ se2_lt_se3
+ se2_ncard_ne_zero
+ se2_subset_units
+ se3
+ se3_subset_se1
+ sp1
+ sp2
+ sp2_le

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@metakunt metakunt changed the title feat(NumberTheory/AksPrimality): Finish claim 1 AKS Primality feat(NumberTheory/AksPrimality): Finish first part of the AKS Primality proof. Jan 28, 2026
kim-em
kim-em reviewed Jan 28, 2026
View reviewed changes
kim-em
kim-em reviewed Jan 28, 2026
View reviewed changes
jcommelin
jcommelin reviewed Jan 28, 2026
View reviewed changes
@jcommelin jcommelin changed the title feat(NumberTheory/AksPrimality): Finish first part of the AKS Primality proof. feat(NumberTheory/AKSPrimality): Finish first part of the AKS Primality proof. Jan 29, 2026
@jcommelin jcommelin changed the title feat(NumberTheory/AKSPrimality): Finish first part of the AKS Primality proof. feat(NumberTheory/AKSPrimality): Finish first part of the AKS Primality proof Jan 29, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 29, 2026 •
edited
Loading

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

vihdzp
vihdzp reviewed Jan 29, 2026
View reviewed changes
@metakunt metakunt marked this pull request as draft January 31, 2026 21:32
@metakunt
Copy link
Copy Markdown
Collaborator Author

metakunt commented Jan 31, 2026

I'll put this as draft until I finish the full theorem. Just wanted to get some feedback first.

@metakunt metakunt changed the title feat(NumberTheory/AKSPrimality): Finish first part of the AKS Primality proof feat(NumberTheory/AKSPrimality): Adds the AKS primality test Feb 27, 2026
qawbecrdtey
qawbecrdtey reviewed Mar 5, 2026
View reviewed changes
@mathlib-triage mathlib-triage bot assigned tb65536 and unassigned kim-em Mar 22, 2026
@tb65536 tb65536 added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 23, 2026
@metakunt
Copy link
Copy Markdown
Collaborator Author

metakunt commented Mar 26, 2026 •
edited
Loading

Thanks for the review @qawbecrdtey. I don't have any naming preferences so I took your suggestions verbatim.

@metakunt metakunt requested a review from qawbecrdtey March 26, 2026 23:48
@metakunt metakunt removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 26, 2026
tb65536
tb65536 reviewed Mar 28, 2026
View reviewed changes
Mathlib/NumberTheory/AKSPrimality.lean Outdated
Comment on lines +57 to +60
/-- The introspective relation, named by the original authors, only used for the construction of the
final theorem, and thus made private. -/
def introspective (f : K[X]) (n : ℕ) (r : ℕ) [NeZero r] : Prop :=
∀ μ ∈ (primitiveRoots r K), f.eval (μ ^ n) = f.eval μ ^ n
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 Mar 28, 2026

Choose a reason for hiding this comment

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

If you're going out of your way to develop API for this, then why not make it public?

Copy link
Copy Markdown
Collaborator Author

@metakunt metakunt Mar 29, 2026

Choose a reason for hiding this comment

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

I've made it public now, although I'm not aware if anyone else has uses for it.

Mathlib/NumberTheory/AKSPrimality.lean
Comment on lines +154 to +168
/-- Helper structure to bundle hypotheses. -/
structure Conditions (r p n a q : ℕ) (μ : K) [Fact p.Prime] [ExpChar K p]
[CharP K p] [NeZero r] where
n_coprime_r : n.Coprime r
n_ge_3 : 3 ≤ n
a_def : a = ⌊(√(φ r) * (Real.logb 2 n))⌋₊
nlogb_lt_od : (Real.logb 2 n) ^ 2 < orderOf (n : ZMod r)
icc_coprime: ∀ y ∈ Icc 1 a, n.Coprime y
icc_introspective: ∀ y : Icc 0 a, introspective ((X : K[X]) - C (y : K)) n r
is_primitive_root : IsPrimitiveRoot μ r
p_prime : p.Prime
q_prime : q.Prime
p_dvd_n : p ∣ n
q_dvd_n : q ∣ n
p_ne_q : p ≠ q
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 Mar 28, 2026

Choose a reason for hiding this comment

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

To me this reads a lot like a technical math paper (here's our list of assumptions throughout the paper, and now we prove a much of technical lemmas). But with formalization there's an opportunity here to re-digest the proof and think about whether there are better ways to phrase the logical flow for Lean, lemmas to extract that could be helpful for the rest of the library. I haven't thought about this proof at all, but it's worth thinking about if you haven't done so already.

Copy link
Copy Markdown
Collaborator Author

@metakunt metakunt Mar 29, 2026

Choose a reason for hiding this comment

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

That is an excellent point. If you read the paper you'll see that the proof is not precise in a sense of being nice to formalise.

Therefore I have done the following simplifications to be easier for a lean workflow.

The reason why I chose this structure was quite simple. Every lemma that I couldn't reasonably extract to the other part of the library should have a straightforward context at the beginning of the proof. I fought with missing instances or just in general with a lot of noise. Setting up the copy paste made grind work without thought.

I definitely agree that if a lemma can be generalised it should with the appropriate hypotheses. Most definitions like f, sp1, se2, etc. seem to only be useful for the context of this proof. I originally inlined them but I wanted explicit irreducibility, so that the infoview is nice and tidy and the easiest and most straightforward way is to just bundle them.

It was the best trade-off I could come up with, considering the section is intended to be private and not exposed. It allowed to fill the context of every lemma with everything I need as well as having consistent, short definition usages and theorem applications.

Mathlib/NumberTheory/AKSPrimality.lean
· exact Coprime.pow_left _ (Coprime.of_dvd_left (div_dvd_of_dvd p_dvd_n) n_coprime_r)
exact ⟨hu.unit, rfl⟩

theorem injective_f (h : Conditions r p n a q μ) : (f h).Injective := by
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 Mar 28, 2026

Choose a reason for hiding this comment

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

For instance, these injectivity results (here and below) could be generalized substantially, I think.

Copy link
Copy Markdown
Collaborator Author

@metakunt metakunt Mar 29, 2026

Choose a reason for hiding this comment

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

What would good generalisations be? For injective_sp1 I could come up with this

theorem injective_sp1_extract {a p : ℕ} {R : Type*} [AddMonoidWithOne R] [CharP R p] (h : a < p)
   : (fun x : Fin (a + 1) ↦ (x.val : R)).Injective := sorry

For injective_f I don't see what a good generalisation would be.

@tb65536 tb65536 added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 28, 2026
@metakunt metakunt removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 29, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 left review comments

+2 more reviewers

@vihdzp vihdzp vihdzp left review comments

@qawbecrdtey qawbecrdtey qawbecrdtey approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@tb65536 tb65536

Labels

t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@metakunt @kim-em @jcommelin @tb65536 @qawbecrdtey @vihdzp