D. J. Bernstein
Proofs
A quite noticeable fraction of my time
is spent on careful manual verification of mathematical proofs;
particularly proofs in papers that I'm publishing, of course,
so that all mistakes are caught.
Tools for automated verification are gradually improving,
and I take advantage of them when I can,
but a large amount of work still needs to be done manually.
My verification procedures have become increasingly systematic,
and in October 2005
I decided to start putting my verification records on the web.
D. J. Bernstein,
``Reducing lattice bases to find small-height values of univariate polynomials,''
ID 82f82c041b7e2bdce94a5e1f94511773:
- Theorem 2.1, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 2.2, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 2.3, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 2.4, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 2.5, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
Relies on
LLL lemma outside the paper:
if m is a positive integer,
and L is a lattice of rank m,
then L has a nonzero vector of length at most 2^((m-1)/2) (det L)^(1/m).
This lemma has the virtue of being polynomial-time constructive;
the ``cost'' theorems in my paper inherit this virtue.
(On the other hand, the virtue is stated only in the accompanying text,
not as part of the theorems.)
- Theorem 2.6, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.1, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.2, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.3, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.4, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.5, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.6, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.7, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 3.8, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 4.1, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 4.2, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 4.3, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 4.4, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 5.1, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 5.2, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 5.3, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 5.4, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 6.1, version 2005.10.09 = 2006.05.31: Proof verified 2005.10.09.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 6.2, version 2005.10.09 = 2006.05.31: Proof verified 2005.10.09.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 6.3, version 2005.10.09 = 2006.05.31: Proof verified 2005.10.09.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 6.4, version 2005.10.09 = 2006.05.31: Proof verified 2005.10.09.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 7.1, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 7.2, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 7.3, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
- Theorem 7.4, version 2006.05.31: Proof verified 2006.05.31.
Version 2007.07.27: Equivalence to version 2006.05.31 verified 2007.07.27.
D. J. Bernstein,
``Curve25519: new Diffie-Hellman speed records,''
ID 4230efdfa673480fc079449d90f322c0:
- Primality of p = 2^255 - 19:
Pocklington-style proof verified 2006.02.09,
using primes
127,
353,
75707,
8574133,
1919519569386763,
75445702479781427272750846543864801,
74058212732561358302231226437062788676166966415465897661863160754340907,
with gp for underlying calculations.
- Non-squareness of 2 and 486662^2-4 in F_p:
Checked 2006.02.09 by gp.
- Primality of p1 = 2^252 + 27742317777372353535851937790883648493:
Pocklington-style proof verified 2006.02.09,
using primes
531581,
1224481,
1257559732178653,
4434155615661930479,
172054593956031949258510691,
19757330305831588566944191468367130476339,
276602624281642239937218680557139826668747,
with gp for underlying calculations.
- Base point (9,...) has order p1:
Checked 2006.02.09 by gp with code
e=ellinit([0,486662,0,1,0]);
u=Mod(9,p);
b=[u,sqrt(u^3+486662*u^2+u)];
ellpow(e,b,p1)==[0].
- Primality of
p2 = (p+1)/2 - 2 p1 = 2^253 - 55484635554744707071703875581767296995:
Pocklington-style proof verified 2006.02.09,
using primes
743104567,
1013266244677,
203852586375664218368381551393371968928013,
104719073621178708975837602950775180438320278101,
27413359092552162435694767700453926735143482401279781,
with gp for underlying calculations.
- (p+1-8p1)^2-4p is divisible by 8312956054562778877481:
Checked 2006.02.09 by gp.
- Order of p mod p1 is (p1-1)/6:
Checked 2006.02.09 by gp.
- Order of p mod p2 is (p2-1)/1:
Checked 2006.02.09 by gp.
- Doubling formulas in version 2006.02.09 produce
lambda^2 - A - 2x = (x^2-1)^2/4y^2 and
y''^2 = x''^3 + A x''^2 + x'':
Verified 2006.02.09.
- Addition formulas in version 2006.02.09 produce
y''^2 = x''^3 + A x''^2 + x'':
Verified 2006.02.09.
- Theorem 2.1, version 2006.02.09:
Proof verified 2006.02.09.
- Theorem B.1, version 2006.02.09:
Proof verified 2006.02.09.
- Theorem B.2, version 2006.02.09:
Proof verified 2006.02.09.