NameDateSize

..20-Nov-20197

AKScleanScript.smlH A D07-Jul-2020116.4 KiB

AKSimprovedScript.smlH A D07-Jul-202081.3 KiB

AKSintroScript.smlH A D07-Jul-2020112.6 KiB

AKSmapsScript.smlH A D07-Jul-2020136.7 KiB

AKSrevisedScript.smlH A D07-Jul-202030.6 KiB

AKSsetsScript.smlH A D07-Jul-202070.8 KiB

AKSshiftScript.smlH A D07-Jul-202017.2 KiB

AKStheoremScript.smlH A D07-Jul-202076 KiB

files.txtH A D20-Nov-20191.6 KiB

HolmakefileH A D20-Nov-2019224

README.mdH A D20-Nov-2019978

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