informath/test/top100.dk at main · GrammaticalFramework/informath · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

Thm01 : (m : Elem Nat) -> (n : Elem Nat) -> Proof (Neq n 0) ->
  Proof (Neq (pow (div m n) 2) 2).
Thm01a : (m : Elem Nat) -> (n : Elem Nat) ->
  Proof (Neq (pow (div m (plus n 1)) 2) 2).
Thm01b : (q : Elem Rat) -> Proof (Neq (pow q 2) 2).
Thm01c : (q : Elem Rat) -> Proof (Neq (sqrt 2) q).

Thm01d : Proof (not (rational (sqrt 2))).

Thm01e : Proof (irrational (sqrt 2)).

Thm01f : Proof (not (exists Nat (p =>
  exists Nat (q => and (Gt q 0) (Eq (square p) (times 2 (square q))))))).

Thm02 : (P : Polynomial) -> Proof (Gt (degree P) 0) ->
  Proof (exists Complex (c => isRoot c P)).

Thm03 : Proof (denumerable Rat).
Thm03a : Proof (Eq (cardinality Nat) (cardinality Rat)).

Thm04 : (u : Elem Vector) -> (v : Elem Vector) -> Proof (orthogonal u v) ->
  Proof (Eq (length (vectorPlus u v)) (sqrt (plus (square (length u)) (square (length v))))).

thm07 : (p : Elem Nat) -> (q : Elem Nat) -> Proof (and (prime p) (prime q)) ->
  Proof (Eq (times (legendre p q) (legendre q p)) (pow (neg 1) (times (div (minus p 1) 2) (div (minus q 1) 2)))).

thm09 : (c : Circle) -> (r : Elem Real) -> Proof (Eq r (radius c)) ->
  Proof (Eq (area c) (times pi (pow r 2))).

thm10FermatLittle : (p : Elem Nat) -> Proof (prime p) -> (a : Elem Int) ->
  Proof (exists Int (q => Eq (minus (pow a p) a) (times p q))).

thm11 : (n : Elem Nat) -> Proof (exists Nat (p => and (Geq p n) (prime p))).

thm19 : (n : Elem Nat) -> Proof (exists Nat (a => exists Nat (b => exists Nat (c => exists Nat (d =>
  Eq n (plus (plus (plus (square a) (square b)) (square c)) (square d))))))).

thm20a : (p : Elem Nat) -> Proof (prime p) -> (k : Elem Nat) -> Proof (Eq p (plus (times 4 k) 1))
  -> Proof (exists Nat (x => exists Nat (y => Eq p (plus (square x) (square y))))).

thm20b : (p : Elem Nat) -> Proof (prime p) -> Proof (congruent p 1 4)
  -> Proof (exists Nat (x => exists Nat (y => Eq p (plus (square x) (square y))))).

thm22 : Proof (not (denumerable Real)).

thm51wilson : (n : Elem Nat) -> Proof (iff (prime n) (congruent (factorial (minus n 1)) (neg 1)  n)).
thm51b : (n : Elem Nat) -> Proof (iff (prime n) (divisible (plus (factorial (minus n 1)) 1) n)).

thm52 : (A : Set) -> Proof (finite A) -> Proof (Eq (cardinality (powerset A)) (pow 2 (cardinality A))).

thm58 : (A : Set) -> (n : Elem Nat) -> Proof (Eq (cardinality A) n) ->
  (k : Elem Nat) -> Proof (Leq k n) ->
    Proof (Eq (cardinality (combinationsFromSet A k)) (binomial n k)).

thm78 : (u : Elem Vector) -> (v : Elem Vector) ->
  Proof (Leq (dotProduct u v) (times (norm u) (norm v))).

thm78a : (u : Elem Vector) -> (v : Elem Vector) ->
  Proof (if (orthogonal u v) (Eq (dotProduct u v) (nd 0))).

thm91 : (u : Elem Vector) -> (v : Elem Vector) ->
  Proof (Leq (norm (vectorPlus u v)) (plus (norm u) (norm v))).

thm98 : (n : Elem Nat) -> Proof (if (Gt n 1) (exists Nat (p => and (prime p) (and (Lt n p) (Lt p (times 2 n)))))).