-
Notifications
You must be signed in to change notification settings - Fork 14
/
existing_proofs.yml
100 lines (100 loc) · 5.71 KB
/
existing_proofs.yml
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
1: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower]
2: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
3: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower]
4: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
5: [HOL Light, Isabelle, Metamath]
6: [Coq (constructive), HOL Light, Isabelle, nqthm]
7: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, nqthm]
8: [HOL Light, Isabelle]
9: [HOL Light, Isabelle, Lean, Metamath, ProofPower]
10: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar]
11: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
12: [HOL Light, Isabelle]
13: [Coq (constructive), HOL Light, Mizar]
14: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
15: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
16: [Coq, Lean]
17: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
18: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar]
19: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS]
20: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
21: [Isabelle]
22: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
23: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
24: [Isabelle, Lean]
25: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
26: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS]
27: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
28: [Coq, HOL Light, Mizar]
29: [Coq (constructive), HOL Light]
30: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
31: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower, nqthm]
32: [Coq]
33: []
34: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
35: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
36: [HOL Light, Isabelle, Mizar]
37: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
38: [ACL2, Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
39: [HOL Light, Isabelle, Lean, Metamath, Mizar]
40: [HOL Light, Isabelle, ProofPower]
41: [Coq, Isabelle]
42: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
43: []
44: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower]
45: [HOL Light, Isabelle, Lean, Metamath, Mizar]
46: [Coq, HOL Light, Isabelle, Metamath, Mizar]
47: [Isabelle]
48: [HOL Light, Isabelle, Metamath]
49: [Coq, HOL Light, Isabelle, Lean, Metamath]
50: [HOL Light]
51: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, nqthm]
52: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
53: [Coq, Isabelle]
54: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
55: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
56: [Coq, Isabelle]
57: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar]
58: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
59: [Coq, Isabelle, Lean]
60: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower]
61: [Coq, HOL Light, Metamath, Mizar]
62: [Coq, Lean]
63: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower]
64: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
65: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
66: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
67: [Coq, HOL Light, Isabelle, Lean, Metamath]
68: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
69: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower]
70: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar]
71: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
72: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS]
73: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
74: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
75: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
76: [HOL Light, Isabelle, Lean, Metamath]
77: [Coq, HOL Light, Isabelle, Lean, Metamath]
78: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
79: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
80: [ACL2, Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower]
81: [HOL Light, Isabelle, Lean, Metamath, ProofPower]
82: [Lean]
83: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar]
84: [Coq, HOL Light, Mizar]
85: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
86: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
87: [Coq, HOL Light, Isabelle, Metamath, Mizar]
88: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
89: [Coq (constructive), HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
90: [Coq, HOL Light, Isabelle, Lean, Metamath]
91: [ACL2, Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower]
92: [HOL Light]
93: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
94: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS]
95: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
96: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
97: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
98: [Coq, HOL Light, Isabelle, Lean, Metamath, Mizar]
99: [Isabelle, ProofPower]
100: [HOL Light, Isabelle, ProofPower]