README.md
1
2# AKS Theories Library
3
4This is a formalisation of the AKS Main Theorem,
5and the implementation of the algorithm in a formalised machine.
6
7## Introspection
8* __AKSintro__, introspective relation for special polynomials and special exponents.
9* __AKSshift__, introspective shifting: from Zn to Zp, where p is a prime.
10* __AKSsets__, introspective sets, for exponents and polynomials.
11* __AKSmaps__, mappings between introspective sets and their shadows.
12
13## The AKS Main Theorem
14* __AKStheorem__, the AKS Main Theorem, with parameter k be prime.
15* __AKSrevised__, the AKS Main Theorem, with parameter k not required to be prime.
16* __AKSimproved__, the AKS Main Theorem, with bounds improved.
17* __AKSclean__, the AKS Main Theorem, a clean version deducing the parameter k.
18
19## AKS Complexity (work in progress)
20* __AKSmachine__, the AKS Machine (still to finish).
21* __AKSextra__, extra stuff: monoids of introspective sets, better lower bound, symbolic polynomials. scalar ring.
22