Tag Archives: computability
Proofs are not programs
A proof, in the sense understood by modern mathematicians, is not always a program. Continue reading
Posted in computability Tagged axiom of choice, bytecode, computability, Curry-Howard 5 Comments
The inverse of a bijection.
Constructing the inverse of a bijection in Lean can be tricky for beginners. Continue reading
Posted in Learning Lean, M1F Tagged computability, M1F 9 Comments