Skip to content

feat(AKS): the word-RAM AKS program and PRIMES ∈ P #1902

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 20 commits into from
Oct 31, 2026
Merged

feat(AKS): the word-RAM AKS program and PRIMES ∈ P #1902

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
fffd3d2
feat(WordRAM/AKS): word-RAM subroutines for the AKS primality test (#…
SamuelSchlesinger Oct 30, 2026
c743e32
feat(WordRAM/AKS): write and compare coefficient arrays (#893)
SamuelSchlesinger Oct 30, 2026
99fd3bc
fix(WordRAM/AKS): wrap long test line and correct two docstrings (#893)
SamuelSchlesinger Oct 31, 2026
a3649ca
feat(WordRAM/AKS): repeated squaring and the congruence test (#893)
SamuelSchlesinger Oct 31, 2026
0f592f2
feat(AKS): integer thresholds, the order search and step 3 (#893)
SamuelSchlesinger Oct 31, 2026
71b9b9c
feat(WordRAM/AKS): the step-5 congruence loop (#893)
SamuelSchlesinger Oct 31, 2026
049074c
Merge remote-tracking branch 'origin/main' into claude/aks-toplevel-893
SamuelSchlesinger Oct 31, 2026
35a8017
feat(WordRAM/AKS): the top-level AKS program and its correctness (#893)
SamuelSchlesinger Oct 31, 2026
6f99f72
Merge remote-tracking branch 'origin/main' into claude/aks-congruence…
SamuelSchlesinger Oct 31, 2026
1b08ead
Merge branch 'claude/aks-congruence-893' into claude/aks-program-893
SamuelSchlesinger Oct 31, 2026
b77e941
Merge branch 'claude/aks-program-893' into claude/aks-toplevel-893
SamuelSchlesinger Oct 31, 2026
b5328a8
chore: add the AKS program to the import aggregate
SamuelSchlesinger Oct 31, 2026
0c9483d
feat(AKS): PRIMES is in P through the word-RAM AKS program (#893)
SamuelSchlesinger Oct 31, 2026
7bf57c7
style(WordRAM/AKS): make a non-terminal simp terminal in the order se…
SamuelSchlesinger Oct 31, 2026
747a514
Merge branch 'claude/aks-program-893' into claude/aks-toplevel-893
SamuelSchlesinger Oct 31, 2026
bf2d042
feat(WordRAM/AKS): the explicit bound time s ≤ 4096 (s + 1)^15 (#893)
SamuelSchlesinger Oct 31, 2026
bd357c7
Merge origin/main into claude/aks-program-893
SamuelSchlesinger Oct 31, 2026
dcc17f6
refactor(AKS): define Passes as PassesUpTo at numTests (#893)
SamuelSchlesinger Oct 31, 2026
69dc7b2
Merge claude/aks-program-893 into claude/aks-toplevel-893
SamuelSchlesinger Oct 31, 2026
c241976
Merge origin/main into claude/aks-toplevel-893
SamuelSchlesinger Oct 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@ public import Complexity.Algorithms.ThreeSum.ChanHe.Sizes
public import Complexity.Algorithms.ThreeSum.Convolution
public import Complexity.Algorithms.ThreeSum.Defs
public import Complexity.Algorithms.ThreeSum.ThreeSets
public import Complexity.Algorithms.WordRAM.AKS
public import Complexity.Algorithms.WordRAM.AKS.Congruence
public import Complexity.Algorithms.WordRAM.AKS.CongruenceLoop
public import Complexity.Algorithms.WordRAM.AKS.GcdTotient
Expand Down Expand Up @@ -1361,6 +1362,7 @@ public import Complexity.Computability.Complexity.Problems.OneInThreeSAT.Reducti
public import Complexity.Computability.Complexity.Problems.Partition
public import Complexity.Computability.Complexity.Problems.PlanarPositiveOneInThreeSAT
public import Complexity.Computability.Complexity.Problems.PlanarThreeSATThree
public import Complexity.Computability.Complexity.Problems.Primes
public import Complexity.Computability.Complexity.Problems.SAT
public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.Drawing
public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingAssembly
Expand Down
Loading
Loading