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 , , , | 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 , | 9 Comments