Advanced: Auditing real theorems🔗

Hands-on audits of famous theorems from Mathlib, from the claim to the verdict, one step and one question at a time.

1. Case 1: Cantor, no list of all subsets
2. Case 2: Euclid: infinitely many primes
3. Case 3: Fermat’s Last Theorem and four fake proofs