TopProver Challenge Log
- ✔ [PASS] #1: plus_assoc
- ✔ [PASS] #2: plus_comm
- ✔ [PASS] #3: 1 + 1 = 2
- ✔ [PASS] #4: forall f: bool -> bool, f^3(x) = f(x)
- ✔ [PASS] #5: n * S m = n + n * m
- ✔ [PASS] #6: n < m / n = m / n > m
- ✔ [PASS] #7: Product of n consecutive integers is divisible by n!
- ✔ [PASS] #8: Equivalent two quicksorts
- ✔ [PASS] #9: forall l: list nat, l @ [0] <> []
- ✔ [PASS] #10: Cumulative sum of list
- ❌ [FAIL] #11: l1 <> l2 if l2 is an odd permutation of l1
- ✔ [PASS] #12: Summand of one
- ✔ [PASS] #13: Definitions of injectivity
- ✔ [PASS] #14: Multiplication in F_2 is idempotent
- ✔ [PASS] #15: Identity permutation
- ✔ [PASS] #16: gcd(n, n+1) = 1
- ✔ [PASS] #17: count l n = count (rev l) n
- ✔ [PASS] #18: unique (unique l) = l
- ✔ [PASS] #19: unique count
- ✔ [PASS] #20: Grand Garden
- ✔ [PASS] #21: mult_n_O
- ✔ [PASS] #22: De Morgan's laws in Coq
- ✔ [PASS] #23: Any natural number is expressible in binary notation
- ✔ [PASS] #24: Multiplication of non-zero value in F_p is injective
- ✔ [PASS] #25: Boolean-hole principle
- ✔ [PASS] #26: Three is prime
- ✔ [PASS] #27: Two is not Three
- ✔ [PASS] #28: Iterated iteration
- ✔ [PASS] #29: Yoneda embedding for preorder
- ✔ [PASS] #30: Double
- ✔ [PASS] #31: Sum of binomial coefficients
- ❌ [PENDING] #32: Uniqueness of inequality proofs
- ✔ [PASS] #33: Constructor is injective
- ✔ [PASS] #34: Tree addressing is injective
- ✔ [PASS] #35: infinite bool sequence is uncountable
- ✔ [PASS] #36: Relative prime squares
- ✔ [PASS] #37: Zero test
- ✔ [PASS] #38: Midpoint
- ✔ [PASS] #39: Boolean-hole principle revisited
- ✔ [PASS] #40: Binary search
- ✔ [PASS] #42: eq_sym?
- ✔ [PASS] #43: Not a sum of squares
- ✔ [PASS] #44: Postorder traversal
- ✔ [PASS] #45: Cycle detection
- ✔ [PASS] #46: Swap twice
- ✔ [PASS] #47: Drinker paradox?
- ✔ [PASS] #48: Upper triangular (soundness)
- ✔ [PASS] #49: Upper triangular (completeness)
- ✔ [PASS] #50: Infinite duplication
- ✔ [PASS] #ex1: Peirce's Law