All problems
- Modus ponens
- Falso
- Peirce
- Converse Peirce
- call/cc
- Sqrt 2
- Induction by tree height
- Seven trees
- PHP
- Increasing sequence 1
- Increasing sequence 2
- Even function
- Prime is decidable
- Ackermann
- Prop to Type
- Increasing sequence 3
- Square Stream
- McCarthy 91 function
- P < EXP
- Collatz conjecture
- Fibonacci function
- Tales of Tails
- Finite Bernstein
- Sum of natural numbers
- Coq.Reals sample
- pi > 3.05
- 8 bits Ascii
- PIE 3
- PIE
- Certified Compiler
- Pell's equation
- Square Lemma
- Perfect square is decidable
- Dirichlet's theorem on arithmetic progressions
- Certified Compressor
- FLT reduction to prime
- Bijective Function 1
- Bijective Function 2
- psatz sample
- Bijective Function 1 (revised)
- JMO2011-3
- snoc_inv
- snoc_inv
- snoc_inv(revised)
- (n+1)^n < n^(n+1)
- (n+1)^n < n^(n+1) (revised)
- GCJJ2011-R1-C
- Certified Brainfuck Echo
- Deduction theorem
- Ackermann function is not primitive recursive
return top