Canonical for Automated Theorem Proving in Lean.

Chase Norman, Jeremy Avigad

Browse the full ITP paper archive.